LeanPool.BruhatTits.Utils.Subring

@[simp]

theorem Subtype.val_comp_single {ι : Type u_1} [DecidableEq ι] {R : Type u_2} [Ring R] {A : Subring R} (i : ι) (a : ↥A) : val ∘ Pi.single i a = Pi.single i ↑a

@[simp]

theorem Subtype.val_comp_add {ι : Type u_1} {R : Type u_2} [Ring R] {A : Subring R} (v w : ι → ↥A) : val ∘ (v + w) = val ∘ v + val ∘ w

@[simp]

theorem Subtype.val_comp_smul {ι : Type u_1} {R : Type u_2} [Ring R] {A : Subring R} (a : ↥A) (v : ι → ↥A) : val ∘ (a • v) = a • val ∘ v

theorem Module.Basis.linearIndependent_of_submodule {ι : Type u_1} {K : Type u_3} [Field K] {R : Subring K} [IsFractionRing (↥R) K] {κ : Type u_4} {M : Submodule (↥R) (ι → K)} (b : Basis κ ↥R ↥M) : LinearIndependent K fun (i : κ) => ↑(b i)