of_basis_left_op — Mathlib

English

If a basis of A is linearly independent over B on the opposite side, then A and B are linearly disjoint.

Русский

Если базис A линейно независим относительно B в противоположном кольце, то A и B линейно несовместны.

LaTeX

$$$\\text{If } a \\text{ is a basis of } A \\text{ with } H, \\ then \\ A \\LinearDisjoint B$$$

Lean4

/-- If a basis of `A` is also `B`-linearly independent in the opposite ring,
then `A` and `B` are linearly disjoint. -/
theorem of_basis_left_op {ι : Type*} (a : Basis ι R A) (H : LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a)) :
    A.LinearDisjoint B := by
  rw [← mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at H
  exact Submodule.LinearDisjoint.of_basis_left _ _ a H

Похожие утверждения