CanonicalBilinear

📁 Source: Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Statistics

Metric	Count
Definitions CoPolarization, CoPolarizationIn, CorootForm, Polarization, PolarizationIn, RootForm, RootFormIn, posRootForm	8
Theorems CoPolarizationIn_apply, CoPolarizationIn_eq, CoPolarization_apply, CoPolarization_eq, PolarizationIn_apply, PolarizationIn_eq, Polarization_apply, algebraMap_posRootForm_posForm, algebraMap_rootFormIn, coPolarization_apply_eq_zero_iff, corootForm_apply_apply, corootForm_self_smul_root, corootSpan_dualAnnihilator_le_ker_rootForm, exists_ge_zero_eq_rootForm, flip_comp_polarization_eq_rootForm, four_nsmul_coPolarization_compl_polarization_apply_root, four_smul_rootForm_sq_eq_coxeterWeight_smul, ker_copolarization_eq_ker_corootForm, ker_polarization_eq_ker_rootForm, pairingIn_le_zero_iff, pairingIn_lt_zero_iff, polarization_apply_eq_zero_iff, posRootForm_eq, posRootForm_posForm_apply_apply, prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, prod_rootForm_smul_coroot_mem_range_domRestrict, range_polarizationIn, range_polarizationIn_le_span_coroot, range_polarization_domRestrict_le_span_coroot, rootFormIn_self_smul_coroot, rootForm_apply_apply, rootForm_reflection_reflection_apply, rootForm_root_self, rootForm_self_smul_coroot, rootForm_self_sum_of_squares, rootForm_symmetric, rootSpan_dualAnnihilator_le_ker_rootForm, self_comp_coPolarization_eq_corootForm, toLinearMap_apply_CoPolarization, toLinearMap_apply_PolarizationIn, toLinearMap_apply_apply_Polarization, zero_le_posForm, zero_lt_pairingIn_iff'	43
Total	51

RootPairing

Definitions

Name	Category	Theorems
CoPolarization 📖	CompOp	9 math math: four_nsmul_coPolarization_compl_polarization_apply_root, coPolarization_apply_eq_zero_iff, self_comp_coPolarization_eq_corootForm, toLinearMap_apply_CoPolarization, ker_copolarization_eq_ker_corootForm, CoPolarizationIn_eq, CoPolarization_apply, CoPolarization_eq, corootForm_self_smul_root
CoPolarizationIn 📖	CompOp	2 math math: CoPolarizationIn_eq, CoPolarizationIn_apply
CorootForm 📖	CompOp	13 math math: four_nsmul_coPolarization_compl_polarization_apply_root, rootSpan_dualAnnihilator_le_ker_rootForm, coPolarization_apply_eq_zero_iff, self_comp_coPolarization_eq_corootForm, toLinearMap_apply_CoPolarization, disjoint_corootSpan_ker_corootForm, ker_copolarization_eq_ker_corootForm, corootForm_apply_apply, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, orthogonal_corootSpan_eq, corootForm_self_smul_root, isCompl_corootSpan_ker_corootForm, ker_corootForm_eq_dualAnnihilator
Polarization 📖	CompOp	15 math math: rootForm_self_smul_coroot, four_nsmul_coPolarization_compl_polarization_apply_root, Polarization_apply, range_polarization_domRestrict_le_span_coroot, finrank_rootSpan_map_polarization_eq_finrank_corootSpan, flip_comp_polarization_eq_rootForm, toLinearMap_apply_apply_Polarization, PolarizationIn_eq, prod_rootForm_smul_coroot_mem_range_domRestrict, polarizationEquiv_apply, range_polarizationIn, polarizationEquiv_toLinearMap, CoPolarization_eq, ker_polarization_eq_ker_rootForm, polarization_apply_eq_zero_iff
PolarizationIn 📖	CompOp	9 math math: finrank_range_polarization_eq_finrank_span_coroot, polarizationIn_Injective, PolarizationIn_eq, toLinearMap_apply_PolarizationIn, PolarizationIn_apply, prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, range_polarizationIn, rootFormIn_self_smul_coroot, range_polarizationIn_le_span_coroot
RootForm 📖	CompOp	33 math math: rootForm_self_smul_coroot, four_nsmul_coPolarization_compl_polarization_apply_root, rootForm_restrict_nondegenerate_of_ordered, coroot_eq_polarizationEquiv_apply_root, rootForm_anisotropic, flip_comp_polarization_eq_rootForm, exists_ge_zero_eq_rootForm, toLinearMap_apply_apply_Polarization, rootForm_root_self, zero_le_rootForm, RootSystem.rootForm_anisotropic, rootForm_reflection_reflection_apply, prod_rootForm_smul_coroot_mem_range_domRestrict, algebraMap_rootFormIn, isCompl_rootSpan_ker_rootForm, rootForm_self_eq_zero_iff, rootForm_apply_apply, rootForm_self_sum_of_squares, algebraMap_posRootForm_posForm, ker_rootForm_eq_dualAnnihilator, polarizationEquiv_symm_apply_coroot, rootForm_restrict_nondegenerate_of_isAnisotropic, rootForm_pos_of_ne_zero, corootSpan_dualAnnihilator_le_ker_rootForm, four_smul_rootForm_sq_eq_coxeterWeight_smul, disjoint_rootSpan_ker_rootForm, rootForm_nondegenerate, toInvariantForm_form, RootSystem.rootForm_nondegenerate, ker_polarization_eq_ker_rootForm, polarization_apply_eq_zero_iff, orthogonal_rootSpan_eq, rootForm_symmetric
RootFormIn 📖	CompOp	6 math math: toLinearMap_apply_PolarizationIn, posRootForm_eq, algebraMap_rootFormIn, prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, rootFormIn_self_smul_coroot, posRootForm_rootFormIn_posDef
posRootForm 📖	CompOp	7 math math: posRootForm_posForm_apply_apply, posRootForm_eq, posRootForm_posForm_pos_of_ne_zero, zero_le_posForm, algebraMap_posRootForm_posForm, posRootForm_posForm_nondegenerate, posRootForm_posForm_anisotropic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
CoPolarizationIn_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike CoPolarizationIn Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Module.Dual NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule root'In Function.Embedding Function.instFunLikeEmbedding root	—	PolarizationIn_apply instIsValuedInFlip
CoPolarizationIn_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike CoPolarizationIn CoPolarization	—	PolarizationIn_eq instIsValuedInFlip
CoPolarization_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike CoPolarization Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Module.Dual NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule root' Function.Embedding Function.instFunLikeEmbedding root	—	Polarization_apply
CoPolarization_eq 📖	mathematical	—	CoPolarization Polarization flip	—	—
PolarizationIn_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike PolarizationIn Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Module.Dual NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule coroot'In Function.Embedding Function.instFunLikeEmbedding coroot	—	LinearMap.coe_sum Finset.sum_congr Finset.sum_apply
PolarizationIn_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module LinearMap.instFunLike PolarizationIn Polarization	—	LinearMap.coe_sum Finset.sum_congr Finset.sum_apply Polarization_apply algebra_compatible_smul algebraMap_coroot'In_apply
Polarization_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Polarization Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Module.Dual NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule coroot' Function.Embedding Function.instFunLikeEmbedding coroot	—	LinearMap.coe_sum Finset.sum_congr Finset.sum_apply
algebraMap_posRootForm_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 root Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPositiveForm.posForm posRootForm RootForm	—	RootPositiveForm.algebraMap_posForm rootForm_symmetric rootForm_reflection_reflection_apply
algebraMap_rootFormIn 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap LinearMap RingHom.id Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootFormIn RootForm	—	LinearMap.coe_sum Finset.sum_congr Finset.sum_apply map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass algebraMap_coroot'In_apply rootForm_apply_apply
coPolarization_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike CoPolarization NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LinearMap.BilinForm NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module CorootForm LinearMap.instZero	—	polarization_apply_eq_zero_iff
corootForm_apply_apply 📖	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 CorootForm Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Module.Dual root'	—	rootForm_apply_apply
corootForm_self_smul_root 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module CorootForm Function.Embedding Function.instFunLikeEmbedding coroot root AddMonoid.toNatSMul CoPolarization	—	rootForm_self_smul_coroot
corootSpan_dualAnnihilator_le_ker_rootForm 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm LinearMap.toPerfPair toLinearMap isPerfPair_toLinearMap Submodule.dualAnnihilator corootSpan LinearMap.ker LinearMap RootForm	—	Algebra.to_smulCommClass RingHomSurjective.ids RingHomInvPair.ids isPerfPair_toLinearMap corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot' LinearMap.ext rootForm_apply_apply Finset.sum_congr MulZeroClass.zero_mul Finset.sum_const_zero
exists_ge_zero_eq_rootForm 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm	—	IsSumSq.nonneg AddGroup.existsAddOfLE FaithfulSMul.algebraMap_injective RootPositiveForm.algebraMap_posForm rootForm_symmetric rootForm_reflection_reflection_apply map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass rootForm_apply_apply IsSumSq.sum_mul_self coroot'_apply_apply_mem_of_mem_span
flip_comp_polarization_eq_rootForm 📖	mathematical	—	LinearMap.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id RingHomCompTriple.ids toLinearMap flip Polarization RootForm	—	LinearMap.ext Algebra.to_smulCommClass RingHomCompTriple.ids Polarization_apply Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.coe_sum Finset.sum_apply rootForm_apply_apply
four_nsmul_coPolarization_compl_polarization_apply_root 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.End.instRing LinearMap.comp RingHomCompTriple.ids CoPolarization Polarization Function.Embedding Function.instFunLikeEmbedding root SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm CorootForm coroot	—	RingHomCompTriple.ids AddMonoid.nat_smulCommClass' LinearMap.smul_apply LinearMap.comp_apply SemigroupAction.mul_smul map_nsmul DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass rootForm_self_smul_coroot map_smul SemilinearMapClass.toMulActionSemiHomClass SMulCommClass.smul_comm AddMonoid.nat_smulCommClass corootForm_self_smul_root smul_smul
four_smul_rootForm_sq_eq_coxeterWeight_smul 📖	mathematical	—	AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm Function.Embedding Function.instFunLikeEmbedding root Algebra.toSMul Algebra.id coxeterWeight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Algebra.to_smulCommClass toLinearMap_apply_apply_Polarization LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul AddCommMonoid.nat_isScalarTower IsScalarTower.right smul_assoc Nat.nsmul_eq_mul LinearMap.IsSymm.eq rootForm_symmetric sq nsmul_eq_mul mul_assoc rootForm_self_smul_coroot smul_mul_assoc mul_smul_comm map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass pairing.eq_1 smul_eq_mul coxeterWeight.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
ker_copolarization_eq_ker_corootForm 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CoPolarization LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module CorootForm	—	ker_polarization_eq_ker_rootForm
ker_polarization_eq_ker_rootForm 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Polarization LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module RootForm	—	Submodule.ext polarization_apply_eq_zero_iff
pairingIn_le_zero_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder pairingIn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne pairingIn_eq_zero_iff le_iff_eq_or_lt pairingIn_lt_zero_iff
pairingIn_lt_zero_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder pairingIn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	pairingIn_reflectionPerm_self_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing pairingIn_reflectionPerm_self_left zero_lt_pairingIn_iff'
polarization_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike Polarization NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LinearMap.BilinForm NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module RootForm LinearMap.instZero	—	Algebra.to_smulCommClass RingHomCompTriple.ids flip_comp_polarization_eq_rootForm map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass RingHomInvPair.ids isPerfPair_toLinearMap EquivLike.toEmbeddingLike SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
posRootForm_eq 📖	mathematical	—	RootPositiveForm.posForm posRootForm RootFormIn	—	LinearMap.ext FaithfulSMul.algebraMap_injective algebraMap_posRootForm_posForm algebraMap_rootFormIn
posRootForm_posForm_apply_apply 📖	mathematical	—	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 root Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPositiveForm.posForm posRootForm Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Module.Dual rootSpan coroot'In	—	FaithfulSMul.algebraMap_injective rootForm_symmetric rootForm_reflection_reflection_apply RootPositiveForm.algebraMap_posForm rootForm_apply_apply Finset.sum_congr map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass algebraMap_coroot'In_apply
prod_rootFormIn_smul_coroot_mem_range_PolarizationIn 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearMap.range rootSpan Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids PolarizationIn SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommRing.toCommMonoid Finset.univ DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootFormIn rootSpanMem Function.Embedding Function.instFunLikeEmbedding coroot	—	RingHomSurjective.ids Finset.dvd_prod_of_mem Finset.mem_univ mul_comm SemigroupAction.mul_smul rootFormIn_self_smul_coroot LinearMap.mem_range IsScalarTower.left Submodule.addSubmonoidClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Nat.instAtLeastTwoHAddOfNat two_smul map_add SemilinearMapClass.toAddHomClass
prod_rootForm_smul_coroot_mem_range_domRestrict 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearMap.range rootSpan Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.domRestrict Polarization SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommRing.toCommMonoid Finset.univ DFunLike.coe LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm Function.Embedding Function.instFunLikeEmbedding root coroot	—	RingHomSurjective.ids Finset.dvd_prod_of_mem Finset.mem_univ mul_comm SemigroupAction.mul_smul rootForm_self_smul_coroot LinearMap.mem_range SMulMemClass.smul_mem Submodule.smulMemClass nsmul_mem Submodule.addSubmonoidClass Submodule.mem_span_of_mem Function.instEmbeddingLikeEmbedding map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul AddCommMonoid.nat_isScalarTower Polarization_apply Finset.sum_congr
range_polarizationIn 📖	mathematical	—	Submodule.map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Polarization rootSpan LinearMap.range Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module PolarizationIn Algebra.id instFaithfulSMul MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instIsValuedIn	—	Submodule.ext RingHomSurjective.ids instFaithfulSMul IsScalarTower.left instIsValuedIn Polarization_apply Finset.sum_congr PolarizationIn_eq
range_polarizationIn_le_span_coroot 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids PolarizationIn corootSpan	—	RingHomSurjective.ids Submodule.mem_span_range_iff_exists_fun PolarizationIn_apply
range_polarization_domRestrict_le_span_coroot 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder LinearMap.range SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.domRestrict Polarization corootSpan	—	RingHomSurjective.ids LinearMap.domRestrict_apply Polarization_apply Submodule.mem_span_range_iff_exists_fun Algebra.to_smulCommClass Finset.sum_congr
rootFormIn_self_smul_coroot 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootFormIn rootSpanMem Function.Embedding Function.instFunLikeEmbedding coroot AddMonoid.toNatSMul PolarizationIn	—	PolarizationIn_apply Finset.sum_congr Fintype.sum_equiv two_nsmul Algebra.to_smulCommClass pairingIn_reflectionPerm pairingIn_reflectionPerm_self_left smul_sub neg_smul sub_neg_eq_add Finset.sum_add_distrib add_assoc sub_eq_iff_eq_add RootFormIn.eq_1 LinearMap.coe_sum Finset.sum_apply Finset.sum_smul Finset.sum_neg_distrib add_neg_cancel algebraMap_pairingIn IsScalarTower.algebraMap_smul SemigroupAction.mul_smul
rootForm_apply_apply 📖	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 RootForm Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Module.Dual coroot'	—	LinearMap.coe_sum Finset.sum_congr Finset.sum_apply
rootForm_reflection_reflection_apply 📖	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 RootForm LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reflection	—	RingHomInvPair.ids rootForm_apply_apply Finset.sum_congr coroot'_reflection Fintype.sum_equiv
rootForm_root_self 📖	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 RootForm Function.Embedding Function.instFunLikeEmbedding root Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib pairing	—	rootForm_apply_apply Finset.sum_congr
rootForm_self_smul_coroot 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm Function.Embedding Function.instFunLikeEmbedding root coroot AddMonoid.toNatSMul Polarization	—	instFaithfulSMul IsScalarTower.left instIsValuedIn Algebra.algebraMap_self_apply rootFormIn_self_smul_coroot PolarizationIn_eq algebraMap_rootFormIn
rootForm_self_sum_of_squares 📖	mathematical	—	IsSumSq Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass 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 RootForm	—	IsSumSq.sum_mul_self rootForm_apply_apply
rootForm_symmetric 📖	mathematical	—	LinearMap.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring RootForm	—	Algebra.to_smulCommClass rootForm_apply_apply Finset.sum_congr map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass mul_comm
rootSpan_dualAnnihilator_le_ker_rootForm 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.map Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module Algebra.to_smulCommClass Algebra.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm LinearMap.toPerfPair toLinearMap flip isPerfPair_toLinearMap Submodule.dualAnnihilator rootSpan LinearMap.ker LinearMap CorootForm	—	corootSpan_dualAnnihilator_le_ker_rootForm
self_comp_coPolarization_eq_corootForm 📖	mathematical	—	LinearMap.comp LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id RingHomCompTriple.ids toLinearMap CoPolarization CorootForm	—	flip_comp_polarization_eq_rootForm
toLinearMap_apply_CoPolarization 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instFunLike toLinearMap CoPolarization LinearMap.BilinForm NonAssocSemiring.toNonUnitalNonAssocSemiring CorootForm	—	LinearMap.ext Algebra.to_smulCommClass toLinearMap_apply_apply_Polarization
toLinearMap_apply_PolarizationIn 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id toLinearMap Submodule SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module PolarizationIn RingHom RingHom.instFunLike algebraMap NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.BilinForm RootFormIn	—	Algebra.to_smulCommClass PolarizationIn_eq algebraMap_rootFormIn toLinearMap_apply_apply_Polarization
toLinearMap_apply_apply_Polarization 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id toLinearMap Polarization NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.BilinForm RootForm	—	Algebra.to_smulCommClass Polarization_apply Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.coe_sum Finset.sum_apply
zero_le_posForm 📖	mathematical	—	Preorder.toLE 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 root Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPositiveForm.posForm posRootForm	—	exists_ge_zero_eq_rootForm FaithfulSMul.algebraMap_injective algebraMap_posRootForm_posForm
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	—	zero_lt_pairingIn_iff

---

← Back to Index