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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.zero Finsupp.instAddCommMonoid Finsupp.module RingHom.id Submodule.mulLeftMap smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid 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	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	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	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	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	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.zero Finsupp.instAddCommMonoid Finsupp.module RingHom.id Submodule.mulRightMap smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid 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.map CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id RingHomSurjective.ids SemilinearMapClass.semilinearMap 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 Matrix.vecCons Matrix.vecEmpty	—	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 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 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.instMin Matrix.vecCons Matrix.vecEmpty	—	not_linearIndependent_pair_of_commute_of_flat mul_comm
not_linearIndependent_pair_of_flat_left 📖	mathematical	Submodule.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	LinearIndependent Submodule 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 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	—	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	—	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	—	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 📖	—	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	—	—	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 📖	—	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	—	—	of_le_left_of_flat of_le_right_of_flat
of_le_of_flat_right 📖	—	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	—	—	of_le_right_of_flat of_le_left_of_flat
of_le_right_of_flat 📖	—	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	—	—	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	—	of_le_left_of_flat one_left
of_linearDisjoint_fg 📖	—	Submodule.LinearDisjoint	—	—	of_linearDisjoint_fg_left of_linearDisjoint_fg_right
of_linearDisjoint_fg_left 📖	—	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 📖	—	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 📖	—	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
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	—	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	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 Cardinal.instOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton 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.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.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.instMin 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 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 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.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 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 📖	—	Submodule.LinearDisjoint Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule SetLike.instMembership Submodule.setLike	—	—	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