LinearDisjoint

📁 Source: Mathlib/RingTheory/LinearDisjoint.lean

Statistics

Metric	Count
Definitions LinearDisjoint, LinearDisjoint, basisOfBasisLeft, basisOfBasisRight, mulMap, mulMapLeftOfSupEqTop, LinearDisjoint	7
Theorems isAlgebraic_of_isField, not_isField_of_transcendental, adjoin_rank_eq_rank_left, adjoin_rank_eq_rank_right, algebraMap_basisOfBasisRight_apply, algebraMap_basisOfBasisRight_repr_apply, basisOfBasisLeft_apply, basisOfBasisLeft_repr_apply, bot_left, bot_right, eq_bot_of_commute_of_self, eq_bot_of_self, exists_field_of_isDomain_of_injective, finrank_sup_of_free, include_range, inf_eq_bot, inf_eq_bot_of_commute, isDomain, isDomain_of_injective, leftMulMatrix_basisOfBasisRight_algebraMap, linearIndependent_left_of_flat, linearIndependent_left_of_flat_of_commute, linearIndependent_left_op_of_flat, linearIndependent_mul_of_flat, linearIndependent_mul_of_flat_left, linearIndependent_mul_of_flat_right, linearIndependent_right_of_flat, map, mulLeftMap_ker_eq_bot_iff_linearIndependent_op, mulMapLeftOfSupEqTop_symm_apply, mulMapLeftOfSupEqTop_tmul, mulRightMap_ker_eq_bot_iff_linearIndependent, norm_algebraMap, of_basis_left, of_basis_left_of_commute, of_basis_left_op, of_basis_mul, of_basis_right, of_finrank_coprime_of_free, of_finrank_sup_of_free, of_isField, of_isField', of_le_left_of_flat, of_le_of_flat_left, of_le_of_flat_right, of_le_right_of_flat, of_linearDisjoint_finite, of_linearDisjoint_finite_left, of_linearDisjoint_finite_right, of_subsingleton, of_subsingleton_top, rank_eq_one_of_commute_of_flat_of_self_of_inj, rank_eq_one_of_flat_of_self_of_inj, rank_inf_eq_one_of_commute_of_flat_left_of_inj, rank_inf_eq_one_of_commute_of_flat_of_inj, rank_inf_eq_one_of_commute_of_flat_right_of_inj, rank_inf_eq_one_of_flat_left_of_inj, rank_inf_eq_one_of_flat_of_inj, rank_inf_eq_one_of_flat_right_of_inj, rank_sup_of_free, sup_free_of_free, symm_of_commute, trace_algebraMap, val_mulMap_tmul, linearDisjoint_comm, linearDisjoint_comm_of_commute, linearDisjoint_iff, linearDisjoint_iff_injective	68
Total	75

Algebra.TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgebraic_of_isField 📖	mathematical	IsField TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring instSemiring	Algebra.IsAlgebraic CommRing.toRing	—	not_isField_of_transcendental
not_isField_of_transcendental 📖	mathematical	—	IsField TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring instSemiring	—	Algebra.injective_of_transcendental includeLeft_injective includeRight_injective Submodule.LinearDisjoint.rank_inf_le_one_of_flat_left Subalgebra.LinearDisjoint.include_range Module.Flat.of_linearEquiv transcendental_iff_injective IsScalarTower.to_smulCommClass' IsScalarTower.of_algHom TensorProduct.CompatibleSMul.isScalarTower RingHom.injective Algebra.to_smulCommClass IsScalarTower.right DivisionRing.isSimpleRing nontrivial_of_algebraMap_injective_of_isDomain Function.Injective.isDomain instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass includeLeft_apply Algebra.adjoin_singleton_eq_range_aeval Algebra.smul_def mul_one Polynomial.aeval_X TensorProduct.smul_tmul IsScalarTower.left LinearMap.lift_rank_le_of_injective Subalgebra.inclusion_injective AlgEquiv.injective Module.Basis.mk_eq_rank commRing_strongRankCondition IsDomain.toNontrivial Cardinal.lift_uzero LE.le.not_gt LE.le.trans Cardinal.mk_eq_aleph0 instCountableNat instInfiniteNat Cardinal.lift_aleph0 Cardinal.one_lt_aleph0

IntermediateField

Definitions

Name	Category	Theorems
LinearDisjoint 📖	MathDef	21 math math: LinearDisjoint.iff_inf_eq_bot, LinearDisjoint.of_basis_right', LinearDisjoint.of_finrank_coprime, LinearDisjoint.of_isField', linearDisjoint_comm, linearDisjoint_iff, LinearDisjoint.bot_left, linearDisjoint_iff', LinearDisjoint.of_basis_mul', LinearDisjoint.of_basis_left, linearDisjoint_comm', LinearDisjoint.of_basis_right, LinearDisjoint.of_inf_eq_bot, linearDisjoint_of_isPurelyInseparable_of_isSeparable, LinearDisjoint.bot_right, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, LinearDisjoint.exists_field_of_isDomain, LinearDisjoint.self_right, LinearDisjoint.of_finrank_sup, LinearDisjoint.of_isField, LinearDisjoint.of_basis_mul

Subalgebra

Definitions

Name	Category	Theorems
LinearDisjoint 📖	MathDef	21 math math: LinearDisjoint.include_range, LinearDisjoint.of_basis_mul, LinearDisjoint.of_basis_left, LinearDisjoint.of_subsingleton, LinearDisjoint.of_isField, LinearDisjoint.of_finrank_coprime_of_free, IntermediateField.linearDisjoint_iff, IntermediateField.linearDisjoint_iff', LinearDisjoint.of_subsingleton_top, LinearDisjoint.exists_field_of_isDomain_of_injective, linearDisjoint_iff, LinearDisjoint.of_finrank_sup_of_free, linearDisjoint_iff_injective, LinearDisjoint.of_basis_left_op, linearDisjoint_comm, LinearDisjoint.of_basis_right, linearDisjoint_comm_of_commute, LinearDisjoint.bot_left, LinearDisjoint.bot_right, LinearDisjoint.of_isField', LinearDisjoint.of_basis_left_of_commute

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 Subalgebra SetLike.instMembership instSetLike	LinearDisjoint	—	LinearDisjoint.symm_of_commute Commute.symm
linearDisjoint_iff 📖	mathematical	—	LinearDisjoint Submodule.LinearDisjoint DFunLike.coe OrderEmbedding Subalgebra Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding toSubmodule	—	—
linearDisjoint_iff_injective 📖	mathematical	—	LinearDisjoint CommSemiring.toSemiring TensorProduct Subalgebra SetLike.instMembership instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toSemiring instModuleSubtypeMem DFunLike.coe AlgHom Algebra.TensorProduct.instSemiring algebra Algebra.TensorProduct.instAlgebra AlgHom.funLike mulMap	—	linearDisjoint_iff Submodule.linearDisjoint_iff

Subalgebra.LinearDisjoint

Definitions

Name	Category	Theorems
basisOfBasisLeft 📖	CompOp	2 math math: basisOfBasisLeft_apply, basisOfBasisLeft_repr_apply
basisOfBasisRight 📖	CompOp	3 math math: algebraMap_basisOfBasisRight_repr_apply, algebraMap_basisOfBasisRight_apply, leftMulMatrix_basisOfBasisRight_algebraMap
mulMap 📖	CompOp	1 math math: val_mulMap_tmul
mulMapLeftOfSupEqTop 📖	CompOp	2 math math: mulMapLeftOfSupEqTop_symm_apply, mulMapLeftOfSupEqTop_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_rank_eq_rank_left 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	Module.rank Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommSemiring Subalgebra.toAlgebra Algebra.id Algebra.adjoin SetLike.coe Subalgebra.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem	—	Subalgebra.rank_toSubmodule Module.Free.rank_eq_card_chooseBasisIndex commRing_strongRankCondition Subalgebra.adjoin_eq_span_basis IsScalarTower.subalgebra' IsScalarTower.right linearIndependent_left_of_flat Module.Basis.linearIndependent rank_span SubsemiringClass.nontrivial Subalgebra.instSubsemiringClass Cardinal.mk_range_eq LinearIndependent.injective
adjoin_rank_eq_rank_right 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	Module.rank Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommSemiring Subalgebra.toAlgebra Algebra.id Algebra.adjoin SetLike.coe Subalgebra.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem	—	adjoin_rank_eq_rank_left symm
algebraMap_basisOfBasisRight_apply 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe Module.Basis SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.moduleLeft Semiring.toModule Module.Basis.instFunLike basisOfBasisRight RingHom Subalgebra.toCommSemiring RingHom.instFunLike algebraMap Subalgebra.toAlgebra Algebra.id Subalgebra.instModuleSubtypeMem	—	RingHomInvPair.ids Module.Basis.baseChange_apply one_mul
algebraMap_basisOfBasisRight_repr_apply 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe RingHom SetLike.instMembership Subalgebra.instSetLike Semiring.toNonAssocSemiring Subalgebra.toCommSemiring RingHom.instFunLike algebraMap Subalgebra.toAlgebra Algebra.id Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Subalgebra.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.instAddCommMonoid Subalgebra.moduleLeft Semiring.toModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basisOfBasisRight Subalgebra.instModuleSubtypeMem	—	RingHomInvPair.ids AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass mulMapLeftOfSupEqTop_symm_apply Module.Basis.baseChange_repr_tmul Algebra.algebraMap_eq_smul_one smul_assoc IsScalarTower.subalgebra' IsScalarTower.right one_smul
basisOfBasisLeft_apply 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe Module.Basis SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.moduleLeft Semiring.toModule Module.Basis.instFunLike basisOfBasisLeft RingHom Subalgebra.toCommSemiring RingHom.instFunLike algebraMap Subalgebra.toAlgebra Algebra.id Subalgebra.instModuleSubtypeMem	—	algebraMap_basisOfBasisRight_apply symm sup_comm
basisOfBasisLeft_repr_apply 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe RingHom SetLike.instMembership Subalgebra.instSetLike Semiring.toNonAssocSemiring Subalgebra.toCommSemiring RingHom.instFunLike algebraMap Subalgebra.toAlgebra Algebra.id Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Subalgebra.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.instAddCommMonoid Subalgebra.moduleLeft Semiring.toModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basisOfBasisLeft Subalgebra.instModuleSubtypeMem	—	algebraMap_basisOfBasisRight_repr_apply symm sup_comm
bot_left 📖	mathematical	—	Subalgebra.LinearDisjoint Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	eq_1 Algebra.toSubmodule_bot Submodule.LinearDisjoint.one_left
bot_right 📖	mathematical	—	Subalgebra.LinearDisjoint Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	eq_1 Algebra.toSubmodule_bot Submodule.LinearDisjoint.one_right
eq_bot_of_commute_of_self 📖	mathematical	Subalgebra.LinearDisjoint Semifield.toCommSemiring Field.toSemifield Ring.toSemiring Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra SetLike.instMembership Subalgebra.instSetLike	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	inf_of_le_left le_refl inf_eq_bot_of_commute
eq_bot_of_self 📖	mathematical	Subalgebra.LinearDisjoint Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring	Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	eq_bot_of_commute_of_self mul_comm
exists_field_of_isDomain_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	AlgHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike Subalgebra.LinearDisjoint AlgHom.range	—	OreLocalization.instIsScalarTower IsScalarTower.right IsFractionRing.injective Localization.isLocalization MonoidHomClass.toMulHomClass Algebra.TensorProduct.includeLeft_injective Algebra.TensorProduct.includeRight_injective AlgHom.range_comp map include_range
finrank_sup_of_free 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	Module.finrank Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass rank_sup_of_free
include_range 📖	mathematical	—	Subalgebra.LinearDisjoint TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra AlgHom.range Algebra.TensorProduct.includeLeft Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.includeRight	—	eq_1 Submodule.linearDisjoint_iff RingHomSurjective.ids RingHomInvPair.ids Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap LinearEquiv.injective
inf_eq_bot 📖	mathematical	Subalgebra.LinearDisjoint Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring	Subalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	inf_eq_bot_of_commute mul_comm
inf_eq_bot_of_commute 📖	mathematical	Subalgebra.LinearDisjoint Semifield.toCommSemiring Field.toSemifield Ring.toSemiring Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Subalgebra.eq_bot_of_rank_le_one commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left Module.Flat.instSubalgebraToSubmodule Module.Flat.of_free Module.Free.of_divisionRing
isDomain 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring	IsDomain TensorProduct Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring Subalgebra.instModuleSubtypeMem Algebra.TensorProduct.instSemiring Subalgebra.algebra	—	Function.Injective.isDomain RingHomClass.toMonoidWithZeroHomClass Algebra.to_smulCommClass IsScalarTower.right RingHom.instRingHomClass Submodule.LinearDisjoint.injective
isDomain_of_injective 📖	mathematical	DFunLike.coe AlgHom CommSemiring.toSemiring AlgHom.funLike Subalgebra.LinearDisjoint AlgHom.range	IsDomain TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring	—	isDomain MulEquiv.isDomain IsScalarTower.to_smulCommClass IsScalarTower.left Subalgebra.instIsScalarTowerSubtypeMem
leftMulMatrix_basisOfBasisRight_algebraMap 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe AlgHom SetLike.instMembership Subalgebra.instSetLike Matrix Subalgebra.toCommSemiring Matrix.semiring Subalgebra.toAlgebra Algebra.id Matrix.instAlgebra AlgHom.funLike Algebra.leftMulMatrix basisOfBasisRight RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Matrix.nonAssocSemiring Subalgebra.toSemiring RingHom.mapMatrix Subalgebra.algebra	—	Matrix.ext RingHomInvPair.ids Algebra.leftMulMatrix_eq_repr_mul algebraMap_basisOfBasisRight_apply algebraMap_basisOfBasisRight_repr_apply
linearIndependent_left_of_flat 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring LinearIndependent Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem	DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Subalgebra.moduleLeft Semiring.toModule	—	linearIndependent_left_of_flat_of_commute mul_comm
linearIndependent_left_of_flat_of_commute 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring LinearIndependent Subalgebra SetLike.instMembership Subalgebra.instSetLike CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Subalgebra.moduleLeft Semiring.toModule	—	linearIndependent_right_of_flat symm_of_commute
linearIndependent_left_op_of_flat 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring LinearIndependent Subalgebra SetLike.instMembership Subalgebra.instSetLike CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem	MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra Subalgebra.op MulOpposite.op DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val MulOpposite.instAddCommMonoid Subalgebra.moduleLeft MulOpposite.instModule Semiring.toOppositeModule	—	smulCommClass_self Algebra.to_smulCommClass Submodule.LinearDisjoint.linearIndependent_left_of_flat Module.Flat.instSubalgebraToSubmodule mulLeftMap_ker_eq_bot_iff_linearIndependent_op
linearIndependent_mul_of_flat 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Module.Flat Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem LinearIndependent CommSemiring.toSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Algebra.toModule	—	Submodule.LinearDisjoint.linearIndependent_mul_of_flat
linearIndependent_mul_of_flat_left 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring LinearIndependent Subalgebra SetLike.instMembership Subalgebra.instSetLike CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Algebra.toModule	—	Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left Module.Flat.instSubalgebraToSubmodule
linearIndependent_mul_of_flat_right 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring LinearIndependent Subalgebra SetLike.instMembership Subalgebra.instSetLike CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Algebra.toModule	—	Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right Module.Flat.instSubalgebraToSubmodule
linearIndependent_right_of_flat 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring LinearIndependent Subalgebra SetLike.instMembership Subalgebra.instSetLike CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem	DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Subalgebra.moduleLeft Semiring.toModule	—	smulCommClass_self IsScalarTower.right Submodule.LinearDisjoint.linearIndependent_right_of_flat Module.Flat.instSubalgebraToSubmodule mulRightMap_ker_eq_bot_iff_linearIndependent
map 📖	mathematical	Subalgebra.LinearDisjoint DFunLike.coe AlgHom AlgHom.funLike	Subalgebra.map	—	Submodule.LinearDisjoint.map
mulLeftMap_ker_eq_bot_iff_linearIndependent_op 📖	mathematical	—	LinearMap.ker Finsupp Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring Algebra.toModule SetLike.instMembership Submodule.setLike DFunLike.coe OrderEmbedding Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule 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 LinearIndependent MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra Subalgebra.instSetLike Subalgebra.op MulOpposite.op AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val MulOpposite.instAddCommMonoid Subalgebra.moduleLeft MulOpposite.instModule Semiring.toOppositeModule	—	smulCommClass_self Algebra.to_smulCommClass AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass RingHomCompTriple.ids RingHomInvPair.ids LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' MulOpposite.instIsScalarTower Subalgebra.isScalarTower_mid IsScalarTower.left IsScalarTower.opposite_mid Finsupp.lhom_ext' LinearMap.ext LinearMap.comp.congr_simp Finsupp.mapRange.linearEquiv_toLinearMap Finsupp.mapRange_single LinearMap.map_zero Finsupp.linearCombination_single Submodule.mulLeftMap_apply_single
mulMapLeftOfSupEqTop_symm_apply 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe AlgEquiv SetLike.instMembership Subalgebra.instSetLike TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring Subalgebra.instModuleSubtypeMem Subalgebra.toCommSemiring Algebra.TensorProduct.instSemiring Subalgebra.algebra Subalgebra.toAlgebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm mulMapLeftOfSupEqTop TensorProduct.tmul OneMemClass.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass	—	Algebra.to_smulCommClass AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass AlgEquiv.symm_apply_eq one_mul
mulMapLeftOfSupEqTop_tmul 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe AlgEquiv SetLike.instMembership Subalgebra.instSetLike TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring Subalgebra.instModuleSubtypeMem Subalgebra.toCommSemiring Algebra.TensorProduct.instSemiring Subalgebra.algebra Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass Subalgebra.toAlgebra AlgEquiv.instFunLike mulMapLeftOfSupEqTop TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Algebra.to_smulCommClass
mulRightMap_ker_eq_bot_iff_linearIndependent 📖	mathematical	—	LinearMap.ker Finsupp Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring Algebra.toModule SetLike.instMembership Submodule.setLike DFunLike.coe OrderEmbedding Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule 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 LinearIndependent Subalgebra.instSetLike AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Subalgebra.moduleLeft Semiring.toModule	—	smulCommClass_self IsScalarTower.right AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' Subalgebra.isScalarTower_mid IsScalarTower.left Finsupp.lhom_ext' LinearMap.ext RingHomCompTriple.ids Finsupp.linearCombination_single Submodule.mulRightMap_apply_single
norm_algebraMap 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe MonoidHom SetLike.instMembership Subalgebra.instSetLike MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing Subalgebra.toCommRing MonoidHom.instFunLike Algebra.norm Subalgebra.toAlgebra Algebra.id RingHom Subalgebra.toCommSemiring RingHom.instFunLike algebraMap Subalgebra.toSemiring Subalgebra.algebra Subalgebra.toRing	—	Algebra.norm_eq_matrix_det Matrix.det.congr_simp leftMulMatrix_basisOfBasisRight_algebraMap RingHom.map_det
of_basis_left 📖	mathematical	LinearIndependent Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Module.Basis NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem Module.Basis.instFunLike Subalgebra.moduleLeft Semiring.toModule	Subalgebra.LinearDisjoint	—	of_basis_left_of_commute mul_comm
of_basis_left_of_commute 📖	mathematical	LinearIndependent Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership Subalgebra.instSetLike DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Module.Basis CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem Module.Basis.instFunLike Subalgebra.moduleLeft Semiring.toModule Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Subalgebra.LinearDisjoint	—	symm_of_commute of_basis_right Commute.symm
of_basis_left_op 📖	mathematical	LinearIndependent MulOpposite Subalgebra CommRing.toCommSemiring MulOpposite.instSemiring Ring.toSemiring MulOpposite.instAlgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.op MulOpposite.op DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Module.Basis CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem Module.Basis.instFunLike MulOpposite.instAddCommMonoid Subalgebra.moduleLeft MulOpposite.instModule Semiring.toOppositeModule	Subalgebra.LinearDisjoint	—	Submodule.LinearDisjoint.of_basis_left smulCommClass_self Algebra.to_smulCommClass mulLeftMap_ker_eq_bot_iff_linearIndependent_op
of_basis_mul 📖	mathematical	LinearIndependent Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership Subalgebra.instSetLike DFunLike.coe Module.Basis CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Subalgebra.toRing Subalgebra.instModuleSubtypeMem Module.Basis.instFunLike Algebra.toModule	Subalgebra.LinearDisjoint	—	Submodule.LinearDisjoint.of_basis_mul
of_basis_right 📖	mathematical	LinearIndependent Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership Subalgebra.instSetLike DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike Subalgebra.val Module.Basis CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem Module.Basis.instFunLike Subalgebra.moduleLeft Semiring.toModule	Subalgebra.LinearDisjoint	—	Submodule.LinearDisjoint.of_basis_right smulCommClass_self IsScalarTower.right mulRightMap_ker_eq_bot_iff_linearIndependent
of_finrank_coprime_of_free 📖	mathematical	Module.finrank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem	Subalgebra.LinearDisjoint	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Subalgebra.eq_bot_of_finrank_one commRing_strongRankCondition bot_right bot_left LinearMap.finrank_le_finrank_of_injective Subalgebra.finite_sup Module.finite_of_finrank_pos Submodule.inclusion_injective of_finrank_sup_of_free LE.le.antisymm Subalgebra.finrank_sup_le_of_free lt_of_lt_of_le Subalgebra.finrank_left_dvd_finrank_sup_of_free Subalgebra.finrank_right_dvd_finrank_sup_of_free
of_finrank_sup_of_free 📖	mathematical	Module.finrank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem	Subalgebra.LinearDisjoint	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim IsScalarTower.to_smulCommClass Subalgebra.instIsScalarTowerSubtypeMem exists_linearIndependent_of_le_finrank Eq.ge Module.finrank_tensorProduct commRing_strongRankCondition RingHomCompTriple.ids RingHomInvPair.ids Module.Free.tensor Module.Free.finsupp Module.Free.self Module.Finite.tensorProduct Module.Finite.finsupp Finite.of_fintype Module.Finite.self Module.finrank_finsupp_self Fintype.card_congr' Fintype.card_fin LinearIndependent.eq_1 Subalgebra.mulMap'_surjective Subalgebra.linearDisjoint_iff Submodule.linearDisjoint_iff Subtype.val_injective OrzechProperty.injective_of_surjective_of_injective CommRing.orzechProperty Subalgebra.finite_sup
of_isField 📖	mathematical	IsField TensorProduct CommRing.toCommSemiring Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem Algebra.TensorProduct.instSemiring Subalgebra.toSemiring Subalgebra.algebra	Subalgebra.LinearDisjoint	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Subalgebra.linearDisjoint_iff_injective RingHom.injective DivisionRing.isSimpleRing
of_isField' 📖	mathematical	IsField TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring Algebra.TensorProduct.instSemiring DFunLike.coe AlgHom CommSemiring.toSemiring AlgHom.funLike	Subalgebra.LinearDisjoint AlgHom.range	—	of_isField MulEquiv.isField IsScalarTower.to_smulCommClass Subalgebra.instIsScalarTowerSubtypeMem IsScalarTower.left
of_le_left_of_flat 📖	—	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder	—	—	Submodule.LinearDisjoint.of_le_left_of_flat Module.Flat.instSubalgebraToSubmodule
of_le_of_flat_left 📖	—	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder	—	—	of_le_left_of_flat of_le_right_of_flat
of_le_of_flat_right 📖	—	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder	—	—	of_le_right_of_flat of_le_left_of_flat
of_le_right_of_flat 📖	—	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder	—	—	Submodule.LinearDisjoint.of_le_right_of_flat Module.Flat.instSubalgebraToSubmodule
of_linearDisjoint_finite 📖	—	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	—	—	of_linearDisjoint_finite_left of_linearDisjoint_finite_right
of_linearDisjoint_finite_left 📖	—	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	—	—	Subalgebra.linearDisjoint_iff Submodule.linearDisjoint_iff RingHomSurjective.ids TensorProduct.exists_finite_submodule_left_of_setFinite' Set.toFinite Finite.Set.finite_insert Finite.of_fintype Submodule.FG.of_finite Submodule.span_le fg_adjoin_of_finite Finset.finite_toSet isIntegral_algHom_iff Subtype.val_injective Algebra.IsIntegral.isIntegral Module.Finite.of_fg Algebra.adjoin_le_iff RingHomCompTriple.ids le_refl LinearMap.range_comp_le_range LinearMap.rTensor_comp Submodule.LinearDisjoint.injective Submodule.mulMap_comp_rTensor
of_linearDisjoint_finite_right 📖	—	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	—	—	symm of_linearDisjoint_finite_left
of_subsingleton 📖	mathematical	—	Subalgebra.LinearDisjoint	—	Submodule.LinearDisjoint.of_subsingleton
of_subsingleton_top 📖	mathematical	—	Subalgebra.LinearDisjoint	—	Submodule.LinearDisjoint.of_subsingleton_top
rank_eq_one_of_commute_of_flat_of_self_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra SetLike.instMembership Subalgebra.instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Module.rank NonUnitalNonAssocSemiring.toAddCommMonoid Subalgebra.toRing Subalgebra.instModuleSubtypeMem Cardinal Cardinal.instOne	—	inf_of_le_left le_refl
rank_eq_one_of_flat_of_self_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Module.rank Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem Cardinal Cardinal.instOne	—	mul_comm
rank_inf_eq_one_of_commute_of_flat_left_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Module.rank NonUnitalNonAssocSemiring.toAddCommMonoid Subalgebra.toRing Subalgebra.instModuleSubtypeMem Cardinal Cardinal.instOne	—	—
rank_inf_eq_one_of_commute_of_flat_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Module.Flat Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Module.rank Cardinal Cardinal.instOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton le_antisymm Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat lift_rank_range_of_injective Cardinal.lift_eq_one Cardinal.lift_one Module.rank_self commRing_strongRankCondition Submodule.rank_mono bot_le
rank_inf_eq_one_of_commute_of_flat_right_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring Ring.toSemiring Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Module.rank NonUnitalNonAssocSemiring.toAddCommMonoid Subalgebra.toRing Subalgebra.instModuleSubtypeMem Cardinal Cardinal.instOne	—	—
rank_inf_eq_one_of_flat_left_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Module.rank Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem Cardinal Cardinal.instOne	—	mul_comm
rank_inf_eq_one_of_flat_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring Module.Flat Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Module.rank SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Cardinal Cardinal.instOne	—	mul_comm
rank_inf_eq_one_of_flat_right_of_inj 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	Module.rank Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem Cardinal Cardinal.instOne	—	mul_comm
rank_sup_of_free 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring	Module.rank Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem Cardinal Cardinal.instMul	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton mul_one IsScalarTower.to_smulCommClass Subalgebra.instIsScalarTowerSubtypeMem rank_tensorProduct' commRing_strongRankCondition LinearEquiv.rank_eq
sup_free_of_free 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring	Module.Free Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring Subalgebra.instModuleSubtypeMem	—	Module.Free.of_equiv Module.Free.tensor Subalgebra.instIsScalarTowerSubtypeMem
symm_of_commute 📖	—	Subalgebra.LinearDisjoint Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra SetLike.instMembership Subalgebra.instSetLike	—	—	Submodule.LinearDisjoint.symm_of_commute
trace_algebraMap 📖	mathematical	Subalgebra.LinearDisjoint CommRing.toCommSemiring CommSemiring.toSemiring Subalgebra SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	DFunLike.coe LinearMap SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommRing RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Subalgebra.toAlgebra Algebra.id Semiring.toModule LinearMap.instFunLike Algebra.trace RingHom Subalgebra.toCommSemiring RingHom.instFunLike algebraMap Subalgebra.toSemiring Subalgebra.algebra	—	Algebra.trace_eq_matrix_trace map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr leftMulMatrix_basisOfBasisRight_algebraMap
val_mulMap_tmul 📖	mathematical	Subalgebra.LinearDisjoint CommSemiring.toSemiring	Subalgebra SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra DFunLike.coe AlgEquiv TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Subalgebra.toSemiring Subalgebra.instModuleSubtypeMem Algebra.TensorProduct.instSemiring Subalgebra.algebra Algebra.TensorProduct.instAlgebra AlgEquiv.instFunLike mulMap TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—

Submodule

Definitions

Name	Category	Theorems
LinearDisjoint 📖	CompData	19 math math: LinearDisjoint.bot_right, LinearDisjoint.of_basis_left', linearDisjoint_iff, LinearDisjoint.one_left, LinearDisjoint.of_basis_mul, LinearDisjoint.of_basis_left, linearDisjoint_comm_of_commute, LinearDisjoint.of_right_le_one_of_flat, Subalgebra.linearDisjoint_iff, LinearDisjoint.of_basis_right', linearDisjoint_op, LinearDisjoint.of_subsingleton_top, linearDisjoint_comm, LinearDisjoint.of_basis_right, LinearDisjoint.of_left_le_one_of_flat, LinearDisjoint.of_basis_mul', LinearDisjoint.one_right, LinearDisjoint.of_subsingleton, LinearDisjoint.bot_left

---

← Back to Index