BaseChange

Statistics

Metric	Count
Definitions	0
Theorems `linearIndependent_algebraMap_comp_iff`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_algebraMap_comp_iff` 📖	mathematical	—	`LinearIndependent` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule`	—	`LinearIndependent.of_comp` `LinearIndependent.restrict_scalars'` `Pi.isScalarTower` `IsScalarTower.right` `IsDomain.of_faithfulSMul` `LinearIndependent.iff_fractionRing` `Localization.isLocalization` `LinearMap.ker_eq_bot` `Submodule.eq_bot_iff` `FractionRing.instFaithfulSMul` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsDomain.toNontrivial` `LinearMap.linearIndependent_iff_of_injOn` `Function.Injective.injOn` `FractionRing.instIsScalarTower` `OreLocalization.instIsScalarTower` `IsScalarTower.left`

---