Theorems · Theorem · commutative algebra

Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op

∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {ι : Type u_1} (a : ι → ↥A),
  (Submodule.mulLeftMap (Subalgebra.toSubmodule B) a).ker = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

2 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra