Linear independence and algebra maps

This file collects results relating linear independence along algebra maps.

These results cannot go in LinearAlgebra/LinearIndependent/Basic.lean due to the algebra import.

@[simp]

theorem LinearIndependent.algebraMap_comp_iff {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [FaithfulSMul S A] {ι : Type u_4} {v : ι → S} : LinearIndependent R (⇑(algebraMap S A) ∘ v) ↔ LinearIndependent R v

@[simp]

theorem LinearIndepOn.algebraMap_comp_iff {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [FaithfulSMul S A] {ι : Type u_4} {v : ι → S} {s : Set ι} : LinearIndepOn R (⇑(algebraMap S A) ∘ v) s ↔ LinearIndepOn R v s

@[simp]

theorem LinearIndepOn.id_image_algebraMap_iff {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] [FaithfulSMul S A] {s : Set S} : LinearIndepOn R id (⇑(algebraMap S A) '' s) ↔ LinearIndepOn R id s