LinearDisjoint

📁 Source: Mathlib/LinearAlgebra/LinearDisjoint.lean

Statistics

Metric	Count
Definitions `mulMap`	1
Theorems `bot_left`, `bot_right`, `injective`, `linearIndependent_left_of_flat`, `linearIndependent_mul_of_flat`, `linearIndependent_mul_of_flat_left`, `linearIndependent_mul_of_flat_right`, `linearIndependent_right_of_flat`, `map`, `not_linearIndependent_pair_of_commute_of_flat`, `not_linearIndependent_pair_of_commute_of_flat_left`, `not_linearIndependent_pair_of_commute_of_flat_right`, `not_linearIndependent_pair_of_flat`, `not_linearIndependent_pair_of_flat_left`, `not_linearIndependent_pair_of_flat_right`, `of_basis_left`, `of_basis_left'`, `of_basis_mul`, `of_basis_mul'`, `of_basis_right`, `of_basis_right'`, `of_le_left_of_flat`, `of_le_of_flat_left`, `of_le_of_flat_right`, `of_le_right_of_flat`, `of_left_le_one_of_flat`, `of_linearDisjoint_fg`, `of_linearDisjoint_fg_left`, `of_linearDisjoint_fg_right`, `of_op`, `of_right_le_one_of_flat`, `of_subsingleton`, `of_subsingleton_top`, `one_left`, `one_right`, `op`, `rank_inf_le_one_of_commute_of_flat`, `rank_inf_le_one_of_commute_of_flat_left`, `rank_inf_le_one_of_commute_of_flat_right`, `rank_inf_le_one_of_flat`, `rank_inf_le_one_of_flat_left`, `rank_inf_le_one_of_flat_right`, `rank_le_one_of_commute_of_flat_of_self`, `rank_le_one_of_flat_of_self`, `symm_of_commute`, `val_mulMap_tmul`, `linearDisjoint_comm`, `linearDisjoint_comm_of_commute`, `linearDisjoint_iff`, `linearDisjoint_op`	50
Total	51

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearDisjoint_comm` 📖	mathematical	—	`LinearDisjoint` `CommSemiring.toSemiring`	—	`LinearDisjoint.symm`
`linearDisjoint_comm_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.instMembership` `setLike`	`LinearDisjoint`	—	`LinearDisjoint.symm_of_commute` `Commute.symm`
`linearDisjoint_iff` 📖	mathematical	—	`LinearDisjoint` `TensorProduct` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `mulMap`	—	—
`linearDisjoint_op` 📖	mathematical	—	`LinearDisjoint` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `DFunLike.coe` `RingEquiv` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule` `MulOpposite.instMul` `mul` `IsScalarTower.right` `MulOpposite.instAdd` `pointwiseAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equivOpposite` `MulOpposite.op`	—	`IsScalarTower.right` `RingHomInvPair.ids` `RingHomCompTriple.ids` `mulMap_op`

Submodule.LinearDisjoint

Definitions

Name	Category	Theorems
`mulMap` 📖	CompOp	1 math math: `val_mulMap_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_left` 📖	mathematical	—	`Submodule.LinearDisjoint` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submodule.instBot`	—	`Function.injective_of_subsingleton` `Unique.instSubsingleton`
`bot_right` 📖	mathematical	—	`Submodule.LinearDisjoint` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submodule.instBot`	—	`Function.injective_of_subsingleton` `Unique.instSubsingleton`
`injective` 📖	mathematical	`Submodule.LinearDisjoint`	`TensorProduct` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `Submodule.mulMap`	—	—
`linearIndependent_left_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `LinearIndependent` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`LinearMap.ker` `Finsupp` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.zero` `Finsupp.instAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `RingHom.id` `Submodule.mulLeftMap` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `CommRing.toRing` `Algebra.to_smulCommClass` `Bot.bot` `Submodule.instBot`	—	`LinearMap.ker_eq_bot_of_injective` `smulCommClass_self` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Submodule.mulLeftMap_eq_mulMap_comp` `injective` `Module.Flat.rTensor_preserves_injective_linearMap` `LinearIndependent.eq_1`
`linearIndependent_mul_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Module.Flat` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `LinearIndependent`	`LinearIndependent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike`	—	`linearIndependent_mul_of_flat_left` `linearIndependent_mul_of_flat_right`
`linearIndependent_mul_of_flat_left` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `LinearIndependent` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`LinearIndependent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike`	—	`LinearIndependent.eq_1` `RingHomInvPair.ids` `RingHomCompTriple.ids` `Module.Flat.rTensor_preserves_injective_linearMap` `Module.Flat.finsupp` `Module.Flat.lTensor_preserves_injective_linearMap` `injective` `LinearEquiv.injective` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `finsuppTensorFinsupp'_symm_single_eq_single_one_tmul` `Finsupp.linearCombination_single` `one_smul`
`linearIndependent_mul_of_flat_right` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `LinearIndependent` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`LinearIndependent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike`	—	`LinearIndependent.eq_1` `RingHomInvPair.ids` `RingHomCompTriple.ids` `Module.Flat.lTensor_preserves_injective_linearMap` `Module.Flat.finsupp` `Module.Flat.rTensor_preserves_injective_linearMap` `injective` `LinearEquiv.injective` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `finsuppTensorFinsupp'_symm_single_eq_single_one_tmul` `Finsupp.linearCombination_single` `one_smul`
`linearIndependent_right_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `LinearIndependent` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`LinearMap.ker` `Finsupp` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.zero` `Finsupp.instAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `RingHom.id` `Submodule.mulRightMap` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `CommRing.toRing` `IsScalarTower.right` `Bot.bot` `Submodule.instBot`	—	`LinearMap.ker_eq_bot_of_injective` `smulCommClass_self` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `Submodule.isScalarTower'` `IsScalarTower.left` `Submodule.mulRightMap_eq_mulMap_comp` `injective` `Module.Flat.lTensor_preserves_injective_linearMap` `LinearIndependent.eq_1`
`map` 📖	mathematical	`Submodule.LinearDisjoint` `DFunLike.coe` `AlgHom` `AlgHom.funLike`	`Submodule.LinearDisjoint` `Submodule.map` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingHom.id` `RingHomSurjective.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`	—	`RingHomSurjective.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Submodule.linearDisjoint_iff` `Function.Injective.of_comp_right` `Submodule.coe_mulMap_comp_eq` `TensorProduct.map_surjective` `LinearMap.submoduleMap_surjective`
`not_linearIndependent_pair_of_commute_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Module.Flat` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Submodule.instMin`	`LinearIndependent` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Matrix.vecCons` `Matrix.vecEmpty` `Submodule.addCommMonoid` `Submodule.module`	—	`not_linearIndependent_pair_of_commute_of_flat_left` `not_linearIndependent_pair_of_commute_of_flat_right`
`not_linearIndependent_pair_of_commute_of_flat_left` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin`	`LinearIndependent` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Matrix.vecCons` `Matrix.vecEmpty` `Submodule.addCommMonoid` `Submodule.module`	—	`inf_le_right` `LinearIndependent.map'` `Submodule.ker_inclusion` `smulCommClass_self` `IsScalarTower.right` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Submodule.mulRightMap_apply_single` `Matrix.cons_val_fin_one` `sub_self` `LinearIndependent.ne_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `ZeroMemClass.coe_eq_zero` `AddSubmonoid.mk_eq_zero` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `Submodule.mem_bot` `linearIndependent_right_of_flat` `LinearMap.mem_ker`
`not_linearIndependent_pair_of_commute_of_flat_right` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin`	`LinearIndependent` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Matrix.vecCons` `Matrix.vecEmpty` `Submodule.addCommMonoid` `Submodule.module`	—	`inf_le_left` `LinearIndependent.map'` `Submodule.ker_inclusion` `smulCommClass_self` `Algebra.to_smulCommClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Submodule.mulLeftMap_apply_single` `Matrix.cons_val_fin_one` `sub_self` `LinearIndependent.ne_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `ZeroMemClass.coe_eq_zero` `AddSubmonoid.mk_eq_zero` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `Submodule.mem_bot` `linearIndependent_left_of_flat` `LinearMap.mem_ker`
`not_linearIndependent_pair_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Module.Flat` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`LinearIndependent` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Matrix.vecCons` `Matrix.vecEmpty` `Submodule.addCommMonoid` `Submodule.module`	—	`not_linearIndependent_pair_of_commute_of_flat` `mul_comm`
`not_linearIndependent_pair_of_flat_left` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`LinearIndependent` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Matrix.vecCons` `Matrix.vecEmpty` `Submodule.addCommMonoid` `Submodule.module`	—	`not_linearIndependent_pair_of_commute_of_flat_left` `mul_comm`
`not_linearIndependent_pair_of_flat_right` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`LinearIndependent` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Matrix.vecCons` `Matrix.vecEmpty` `Submodule.addCommMonoid` `Submodule.module`	—	`not_linearIndependent_pair_of_commute_of_flat_right` `mul_comm`
`of_basis_left` 📖	mathematical	`LinearMap.ker` `Finsupp` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.zero` `Finsupp.instAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `RingHom.id` `Submodule.mulLeftMap` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `CommRing.toRing` `Algebra.to_smulCommClass` `DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `Bot.bot` `Submodule.instBot`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `of_basis_left'` `LinearMap.ker_eq_bot`
`of_basis_left'` 📖	mathematical	`Finsupp` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.zero` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `LinearMap.instFunLike` `Submodule.mulLeftMap` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Module.Basis` `Module.Basis.instFunLike`	`Submodule.LinearDisjoint`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.comp.congr_simp` `Submodule.mulLeftMap_eq_mulMap_comp`
`of_basis_mul` 📖	mathematical	`LinearIndependent` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `Module.Basis` `Submodule.addCommMonoid` `Submodule.module` `Module.Basis.instFunLike`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`of_basis_mul'` `LinearIndependent.eq_1`
`of_basis_mul'` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Algebra.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Module.Basis` `Submodule.addCommMonoid` `Submodule.module` `Module.Basis.instFunLike`	`Submodule.LinearDisjoint`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `finsuppTensorFinsupp'_symm_single_eq_single_one_tmul` `Module.Basis.repr_symm_apply` `Finsupp.linearCombination_single` `one_smul`
`of_basis_right` 📖	mathematical	`LinearMap.ker` `Finsupp` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.zero` `Finsupp.instAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `RingHom.id` `Submodule.mulRightMap` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `CommRing.toRing` `IsScalarTower.right` `DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `Bot.bot` `Submodule.instBot`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`smulCommClass_self` `IsScalarTower.right` `of_basis_right'` `LinearMap.ker_eq_bot`
`of_basis_right'` 📖	mathematical	`Finsupp` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.zero` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Submodule.module` `LinearMap.instFunLike` `Submodule.mulRightMap` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.right` `Module.Basis` `Module.Basis.instFunLike`	`Submodule.LinearDisjoint`	—	`smulCommClass_self` `IsScalarTower.right` `RingHomInvPair.ids` `RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass` `Submodule.isScalarTower'` `IsScalarTower.left` `LinearMap.comp.congr_simp` `Submodule.mulRightMap_eq_mulMap_comp`
`of_le_left_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`RingHomCompTriple.ids` `injective` `Module.Flat.rTensor_preserves_injective_linearMap` `Submodule.inclusion_injective` `TensorProduct.AlgebraTensorModule.curry_injective` `Submodule.isScalarTower'` `IsScalarTower.left` `LinearMap.ext` `IsScalarTower.to_smulCommClass`
`of_le_of_flat_left` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`of_le_left_of_flat` `of_le_right_of_flat`
`of_le_of_flat_right` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`of_le_right_of_flat` `of_le_left_of_flat`
`of_le_right_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`RingHomCompTriple.ids` `injective` `Module.Flat.lTensor_preserves_injective_linearMap` `Submodule.inclusion_injective` `TensorProduct.AlgebraTensorModule.curry_injective` `Submodule.isScalarTower'` `IsScalarTower.left` `LinearMap.ext` `IsScalarTower.to_smulCommClass`
`of_left_le_one_of_flat` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.one`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`of_le_left_of_flat` `one_left`
`of_linearDisjoint_fg` 📖	mathematical	`Submodule.LinearDisjoint`	`Submodule.LinearDisjoint`	—	`of_linearDisjoint_fg_left` `of_linearDisjoint_fg_right`
`of_linearDisjoint_fg_left` 📖	mathematical	`Submodule.LinearDisjoint`	`Submodule.LinearDisjoint`	—	`Submodule.linearDisjoint_iff` `RingHomSurjective.ids` `TensorProduct.exists_finite_submodule_left_of_setFinite'` `Set.toFinite` `Finite.Set.finite_insert` `Finite.of_fintype` `injective` `Module.Finite.iff_fg` `RingHomCompTriple.ids` `Submodule.mulMap_comp_rTensor`
`of_linearDisjoint_fg_right` 📖	mathematical	`Submodule.LinearDisjoint`	`Submodule.LinearDisjoint`	—	`Submodule.linearDisjoint_iff` `RingHomSurjective.ids` `TensorProduct.exists_finite_submodule_right_of_setFinite'` `Set.toFinite` `Finite.Set.finite_insert` `Finite.of_fintype` `injective` `Module.Finite.iff_fg` `RingHomCompTriple.ids` `Submodule.mulMap_comp_lTensor`
`of_op` 📖	mathematical	`Submodule.LinearDisjoint` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `DFunLike.coe` `RingEquiv` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule` `MulOpposite.instMul` `Submodule.mul` `IsScalarTower.right` `MulOpposite.instAdd` `Submodule.pointwiseAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `Submodule.equivOpposite` `MulOpposite.op`	`Submodule.LinearDisjoint`	—	`IsScalarTower.right` `Submodule.linearDisjoint_op`
`of_right_le_one_of_flat` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.one`	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`of_le_right_of_flat` `one_right`
`of_subsingleton` 📖	mathematical	—	`Submodule.LinearDisjoint`	—	`Function.injective_of_subsingleton` `Unique.instSubsingleton` `instSubsingletonSubtype_mathlib` `Module.subsingleton`
`of_subsingleton_top` 📖	mathematical	—	`Submodule.LinearDisjoint`	—	`Function.injective_of_subsingleton` `Unique.instSubsingleton` `instSubsingletonSubtype_mathlib`
`one_left` 📖	mathematical	—	`Submodule.LinearDisjoint` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submodule.one`	—	`Submodule.linearDisjoint_iff` `Algebra.toSubmodule_bot` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Submodule.mulMap_one_left_eq` `Submodule.injective_subtype` `LinearEquiv.injective`
`one_right` 📖	mathematical	—	`Submodule.LinearDisjoint` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Submodule.one`	—	`Submodule.linearDisjoint_iff` `Algebra.toSubmodule_bot` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Submodule.mulMap_one_right_eq` `Submodule.injective_subtype` `LinearEquiv.injective`
`op` 📖	mathematical	`Submodule.LinearDisjoint`	`Submodule.LinearDisjoint` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `DFunLike.coe` `RingEquiv` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule` `MulOpposite.instMul` `Submodule.mul` `IsScalarTower.right` `MulOpposite.instAdd` `Submodule.pointwiseAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `Submodule.equivOpposite` `MulOpposite.op`	—	`IsScalarTower.right` `Submodule.linearDisjoint_op`
`rank_inf_le_one_of_commute_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Module.Flat` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Submodule.instMin`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `rank_subsingleton` `instReflLe` `rank_le` `Nontrivial.exists_pair_ne` `Fintype.one_lt_card_iff_nontrivial` `Fintype.card_coe` `not_le` `not_linearIndependent_pair_of_commute_of_flat` `LinearIndependent.comp` `Fintype.complete` `Matrix.cons_val_fin_one`
`rank_inf_le_one_of_commute_of_flat_left` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`rank_inf_le_one_of_commute_of_flat`
`rank_inf_le_one_of_commute_of_flat_right` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`rank_inf_le_one_of_commute_of_flat`
`rank_inf_le_one_of_flat` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Module.Flat` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`rank_inf_le_one_of_commute_of_flat` `mul_comm`
`rank_inf_le_one_of_flat_left` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`rank_inf_le_one_of_commute_of_flat_left` `mul_comm`
`rank_inf_le_one_of_flat_right` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.instMin` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`rank_inf_le_one_of_commute_of_flat_right` `mul_comm`
`rank_le_one_of_commute_of_flat_of_self` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `Ring.toSemiring` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`inf_of_le_left` `le_refl` `rank_inf_le_one_of_commute_of_flat_left`
`rank_le_one_of_flat_of_self` 📖	mathematical	`Submodule.LinearDisjoint` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	`rank_le_one_of_commute_of_flat_of_self` `mul_comm`
`symm_of_commute` 📖	mathematical	`Submodule.LinearDisjoint` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike`	`Submodule.LinearDisjoint`	—	`Submodule.linearDisjoint_iff` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Submodule.mulMap_comm_of_commute` `Algebra.to_smulCommClass` `IsScalarTower.right` `Equiv.injective_comp` `injective`
`val_mulMap_tmul` 📖	mathematical	`Submodule.LinearDisjoint`	`Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.mul` `IsScalarTower.right` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct` `Submodule.addCommMonoid` `Submodule.module` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `mulMap` `TensorProduct.tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsScalarTower.right` `RingHomInvPair.ids`

---

← Back to Index