RootPositive

📁 Source: Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

Statistics

Metric	Count
Definitions form, RootPositiveForm, form, posForm, rootLength, toInvariantForm	6
Theorems apply_reflection_reflection, apply_root_ne_zero, apply_root_root_zero_iff, isOrthogonal_reflection, ne_zero, pairing_mul_eq_pairing_mul_swap, two_mul_apply_root_root, algebraMap_apply_eq_form_iff, algebraMap_posForm, algebraMap_rootLength, exists_eq, exists_pos_eq, form_apply_root_ne_zero, isOrthogonal_reflection, isSymm_posForm, pairingIn_mul_eq_pairingIn_mul_swap, posForm_apply_root_root_le_zero_iff, rootLength_pos, rootLength_reflectionPerm_self, toInvariantForm_form, two_mul_apply_root_root, zero_lt_apply_root_root_iff, zero_lt_posForm_apply_root, zero_lt_posForm_iff, coxeterWeight_nonneg, zero_lt_pairingIn_iff	26
Total	32

RootPairing

Definitions

Name	Category	Theorems
RootPositiveForm 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coxeterWeight_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing coxeterWeightIn	—	lt_or_ge le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono zero_lt_pairingIn_iff not_lt mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
zero_lt_pairingIn_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing pairingIn	—	Submodule.subset_span Set.mem_range_self RootPositiveForm.zero_lt_apply_root_root_iff Algebra.to_smulCommClass LinearMap.IsSymm.eq RootPositiveForm.isSymm_posForm RingHom.id_apply

RootPairing.InvariantForm

Definitions

Name	Category	Theorems
form 📖	CompOp	20 math math: apply_reflection_reflection, RootPairing.EmbeddedG2.shortAddLongRoot_shortRoot, pairing_mul_eq_pairing_mul_swap, symm, exists_apply_eq_or, isOrthogonal_reflection, RootPairing.EmbeddedG2.long_eq_three_mul_short, apply_weylGroup_smul, apply_eq_or_aux, RootPairing.RootPositiveForm.toInvariantForm_form, RootPairing.exists_form_eq_form_and_form_ne_zero, apply_root_root_zero_iff, apply_eq_or, RootPairing.EmbeddedG2.twoShortAddLongRoot_shortRoot, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, apply_eq_or_of_apply_ne, two_mul_apply_root_root, RootPairing.EmbeddedG2.threeShortAddLongRoot_longRoot, RootPairing.toInvariantForm_form, RootPairing.EmbeddedG2.threeShortAddTwoLongRoot_longRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_reflection_reflection 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv RootPairing.reflection	—	isOrthogonal_reflection
apply_root_ne_zero 📖	—	—	—	—	ne_zero
apply_root_root_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Function.Embedding Function.instFunLikeEmbedding RootPairing.root MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RootPairing.pairing	—	Nat.instAtLeastTwoHAddOfNat IsDomain.to_noZeroDivisors two_mul_apply_root_root ne_zero
isOrthogonal_reflection 📖	mathematical	—	LinearMap.IsOrthogonal form DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv RootPairing.reflection	—	—
ne_zero 📖	—	—	—	—	—
pairing_mul_eq_pairing_mul_swap 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RootPairing.pairing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	Nat.instAtLeastTwoHAddOfNat two_mul_apply_root_root Algebra.to_smulCommClass LinearMap.IsSymm.eq symm RingHom.id_apply
two_mul_apply_root_root 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Function.Embedding Function.instFunLikeEmbedding RootPairing.root RootPairing.pairing	—	Nat.instAtLeastTwoHAddOfNat two_mul eq_sub_iff_add_eq RingHomInvPair.ids isOrthogonal_reflection RootPairing.reflection_apply RootPairing.reflection_apply_self RootPairing.root_coroot'_eq_pairing LinearMap.map_sub₂ LinearMap.map_smul₂ smul_eq_mul map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass mul_neg neg_sub_neg

RootPairing.RootPositiveForm

Definitions

Name	Category	Theorems
form 📖	CompOp	10 math math: algebraMap_rootLength, zero_lt_posForm_iff, exists_eq, isOrthogonal_reflection, symm, two_mul_apply_root_root, toInvariantForm_form, exists_pos_eq, algebraMap_apply_eq_form_iff, algebraMap_posForm
posForm 📖	CompOp	14 math math: RootPairing.posRootForm_posForm_apply_apply, zero_lt_posForm_apply_root, zero_lt_posForm_iff, posForm_apply_root_root_le_zero_iff, RootPairing.posRootForm_eq, RootPairing.posRootForm_posForm_pos_of_ne_zero, RootPairing.zero_le_posForm, RootPairing.algebraMap_posRootForm_posForm, isSymm_posForm, RootPairing.posRootForm_posForm_nondegenerate, algebraMap_apply_eq_form_iff, zero_lt_apply_root_root_iff, RootPairing.posRootForm_posForm_anisotropic, algebraMap_posForm
rootLength 📖	CompOp	6 math math: algebraMap_rootLength, pairingIn_mul_eq_pairingIn_mul_swap, rootLength_pos, rootLength_reflectionPerm_self, rootLength_le_of_pairingIn_eq, rootLength_lt_of_pairingIn_notMem
toInvariantForm 📖	CompOp	1 math math: toInvariantForm_form

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_apply_eq_form_iff 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap LinearMap RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Submodule SetLike.instMembership Submodule.setLike Submodule.span Set.range Function.Embedding Function.instFunLikeEmbedding RootPairing.root Submodule.addCommMonoid Submodule.module posForm	—	smulCommClass_self
algebraMap_posForm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap LinearMap RingHom.id Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range Function.Embedding Function.instFunLikeEmbedding RootPairing.root Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module posForm form	—	smulCommClass_self LinearMap.restrictScalarsRange₂_apply
algebraMap_rootLength 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap rootLength LinearMap RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	algebraMap_posForm
exists_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap LinearMap RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	—
exists_pos_eq 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap LinearMap RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	—
form_apply_root_ne_zero 📖	—	—	—	—	exists_pos_eq LT.lt.ne'
isOrthogonal_reflection 📖	mathematical	—	LinearMap.IsOrthogonal form DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv RootPairing.reflection	—	—
isSymm_posForm 📖	mathematical	—	LinearMap.IsSymm Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring posForm	—	FaithfulSMul.algebraMap_injective Algebra.to_smulCommClass algebraMap_posForm LinearMap.IsSymm.eq symm
pairingIn_mul_eq_pairingIn_mul_swap 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RootPairing.pairingIn rootLength	—	FaithfulSMul.algebraMap_injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass RootPairing.algebraMap_pairingIn algebraMap_rootLength RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swap
posForm_apply_root_root_le_zero_iff 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Submodule.subset_span Set.mem_range_self	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module posForm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RootPairing.pairingIn	—	not_iff_not not_le Submodule.subset_span Set.mem_range_self zero_lt_apply_root_root_iff
rootLength_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing rootLength	—	zero_lt_posForm_apply_root Submodule.subset_span Set.mem_range_self
rootLength_reflectionPerm_self 📖	mathematical	—	rootLength DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike RootPairing.reflectionPerm	—	AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass RootPairing.rootSpanMem_reflectionPerm_self map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_neg
toInvariantForm_form 📖	mathematical	—	RootPairing.InvariantForm.form toInvariantForm form	—	—
two_mul_apply_root_root 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module form Function.Embedding Function.instFunLikeEmbedding RootPairing.root RootPairing.pairing	—	RootPairing.InvariantForm.two_mul_apply_root_root
zero_lt_apply_root_root_iff 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Submodule.subset_span Set.mem_range_self	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module posForm RootPairing.pairingIn	—	Nat.instAtLeastTwoHAddOfNat FaithfulSMul.algebraMap_injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_ofNat algebraMap_posForm RootPairing.algebraMap_pairingIn RootPairing.InvariantForm.two_mul_apply_root_root mul_pos_iff_of_pos_left IsStrictOrderedRing.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE zero_lt_two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Submodule.subset_span Set.mem_range_self mul_pos_iff_of_pos_right IsStrictOrderedRing.toMulPosStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE zero_lt_posForm_apply_root
zero_lt_posForm_apply_root 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Submodule.subset_span Set.mem_range_self	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module posForm	—	exists_pos_eq
zero_lt_posForm_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range Function.Embedding Function.instFunLikeEmbedding RootPairing.root Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module posForm RingHom RingHom.instFunLike algebraMap form	—	algebraMap_posForm FaithfulSMul.algebraMap_injective

---

← Back to Index