Nondegenerate

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

Statistics

Metric	Count
Definitions Nondegenerate, Nondegenerate, Nondegenerate, IsAnisotropic, PolarizationEquiv, toInvariantForm	6
Theorems Nondegenerate, corootForm_coroot_ne_zero, rootForm_root_ne_zero, coroot_eq_polarizationEquiv_apply_root, disjoint_corootSpan_ker_corootForm, disjoint_rootSpan_ker_rootForm, eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero, exists_coroot_ne, finrank_corootSpan_eq, finrank_corootSpan_eq', finrank_range_polarization_eq_finrank_span_coroot, finrank_rootSpan_map_polarization_eq_finrank_corootSpan, instIsAnisotropicFlip, instIsAnisotropicOfIsCrystallographic, instIsAnisotropicOfLinearOrderedCommRing, instIsBalanced, isAnisotropic_of_isValuedIn, isCompl_corootSpan_ker_corootForm, isCompl_rootSpan_ker_rootForm, ker_corootForm_eq_dualAnnihilator, ker_rootForm_eq_dualAnnihilator, linearIndepOn_coroot_iff, orthogonal_corootSpan_eq, orthogonal_rootSpan_eq, polarizationEquiv_apply, polarizationEquiv_symm_apply_coroot, polarizationEquiv_toLinearMap, polarizationIn_Injective, posRootForm_posForm_anisotropic, posRootForm_posForm_nondegenerate, posRootForm_posForm_pos_of_ne_zero, posRootForm_rootFormIn_posDef, rootForm_anisotropic, rootForm_nondegenerate, rootForm_pos_of_ne_zero, rootForm_restrict_nondegenerate_of_isAnisotropic, rootForm_restrict_nondegenerate_of_ordered, rootForm_self_eq_zero_iff, rootSpan_eq_top_iff, smul_coroot_eq_of_root_add_root_eq, toInvariantForm_form, zero_le_rootForm, rootForm_anisotropic, rootForm_nondegenerate	44
Total	50

Configuration

Definitions

Name	Category	Theorems
Nondegenerate 📖	CompData	4 math math: Dual.Nondegenerate, HasLines.toNondegenerate, ofField.instNondegenerateProjectivizationForallFinOfNatNat, HasPoints.toNondegenerate

Configuration.Dual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Nondegenerate 📖	mathematical	—	Configuration.Nondegenerate Configuration.Dual Configuration.instMembershipDual	—	Configuration.Nondegenerate.exists_line Configuration.Nondegenerate.exists_point Configuration.Nondegenerate.eq_or_eq

LinearMap

Definitions

Name	Category	Theorems
Nondegenerate 📖	MathDef	27 math math: RootPairing.rootForm_restrict_nondegenerate_of_ordered, nondegenerate_toLinearMap₂'_of_det_ne_zero', Matrix.Nondegenerate.toLinearMap₂, nondegenerate_of_det_ne_zero, Submodule.quotDualCoannihilatorToDual_nondegenerate, BilinForm.nondegenerate_iff, Subspace.dualPairing_nondegenerate, BilinForm.nondegenerate_iff', nondegenerate_iff_det_ne_zero, dualPairing_nondegenerate, IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self, BilinForm.nondegenerate_restrict_iff_disjoint_ker, nondegenerate_congr_iff, Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, Matrix.nondegenerate_toLinearMap₂_iff, nondegenerate_toMatrix₂'_iff, nondegenerate_toLinearMap₂'_iff_det_ne_zero, flip_nondegenerate, Subspace.dualCopairing_nondegenerate, IsSymm.nondegenerate_restrict_of_isCompl_ker, RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic, nondegenerate_toMatrix₂_iff, Matrix.nondegenerate_toLinearMap₂'_iff, nondegenerate_restrict_of_disjoint_orthogonal, IsRefl.nondegenerate_iff_separatingLeft, IsRefl.nondegenerate_iff_separatingRight, Matrix.Nondegenerate.toLinearMap₂'

LinearMap.BilinForm

Definitions

Name	Category	Theorems
Nondegenerate 📖	MathDef	29 math math: Nondegenerate.ofSeparatingRight, traceForm_nondegenerate_tfae, LieAlgebra.IsKilling.traceForm_cartan_nondegenerate, nondegenerate_flip_iff, restrict_nondegenerate_iff_isCompl_orthogonal, nondegenerate_toMatrix_iff, Matrix.nondegenerate_toBilin'_iff, not_nondegenerate_zero, Nondegenerate.ofSeparatingLeft, LieAlgebra.IsKilling.killingForm_nondegenerate, Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, Matrix.nondegenerate_toBilin_iff, Matrix.Nondegenerate.toBilin, nondegenerate_toBilin'_iff_det_ne_zero, nondegenerate_iff_ker_eq_bot, nondegenerate_toMatrix'_iff, nondegenerate_of_det_ne_zero, nondegenerate_congr_iff, RootPairing.posRootForm_posForm_nondegenerate, traceForm_nondegenerate, nonDegenerateFlip_iff, Matrix.Nondegenerate.toBilin', RootPairing.rootForm_nondegenerate, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, nondegenerate_toBilin'_of_det_ne_zero', nondegenerate_iff_det_ne_zero, RootSystem.rootForm_nondegenerate, nondegenerate_restrict_of_disjoint_orthogonal, iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self

RootPairing

Definitions

Name	Category	Theorems
IsAnisotropic 📖	CompData	4 math math: instIsAnisotropicOfLinearOrderedCommRing, instIsAnisotropicOfIsCrystallographic, instIsAnisotropicFlip, isAnisotropic_of_isValuedIn
PolarizationEquiv 📖	CompOp	4 math math: coroot_eq_polarizationEquiv_apply_root, polarizationEquiv_apply, polarizationEquiv_toLinearMap, polarizationEquiv_symm_apply_coroot
toInvariantForm 📖	CompOp	1 math math: toInvariantForm_form

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coroot_eq_polarizationEquiv_apply_root 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding coroot EuclideanDomain.toCommRing Field.toEuclideanDomain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Nat.instAtLeastTwoHAddOfNat LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm root LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv PolarizationEquiv	—	IsAnisotropic.rootForm_root_ne_zero Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids polarizationEquiv_apply smul_right_injective instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero rootForm_self_smul_coroot smul_smul mul_div_cancel₀ Nat.cast_smul_eq_nsmul
disjoint_corootSpan_ker_corootForm 📖	mathematical	—	Disjoint Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder Submodule.instOrderBot corootSpan LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module CorootForm	—	disjoint_rootSpan_ker_rootForm instIsAnisotropicFlip
disjoint_rootSpan_ker_rootForm 📖	mathematical	—	Disjoint Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder Submodule.instOrderBot rootSpan LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module RootForm	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap ker_polarization_eq_ker_rootForm Submodule.disjoint_ker_of_finrank_le IsDomain.hasRankNullity commRing_strongRankCondition IsDomain.toNontrivial Module.IsReflexive.to_isTorsionFree instFiniteSubtypeMemSubmoduleRootSpanOfFinite Finite.of_fintype RingHomSurjective.ids finrank_rootSpan_map_polarization_eq_finrank_corootSpan finrank_corootSpan_eq' le_refl
eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	rootForm_self_eq_zero_iff Disjoint.eq_bot disjoint_rootSpan_ker_rootForm IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE instIsAnisotropicOfLinearOrderedCommRing
exists_coroot_ne 📖	—	—	—	—	polarizationIn_Injective map_ne_zero_iff AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Mathlib.Tactic.Contrapose.contrapose₂ Fintype.sum_eq_zero zero_smul PolarizationIn_apply
finrank_corootSpan_eq 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan Submodule.addCommMonoid Submodule.module rootSpan	—	le_antisymm instIsValuedInFlip instIsAnisotropicFlip
finrank_corootSpan_eq' 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike corootSpan Submodule.addCommMonoid Submodule.module rootSpan	—	le_antisymm instIsAnisotropicFlip
finrank_range_polarization_eq_finrank_span_coroot 📖	mathematical	—	Module.finrank 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 corootSpan	—	LE.le.antisymm RingHomSurjective.ids Submodule.finrank_mono commRing_strongRankCondition IsDomain.toNontrivial instFiniteSubtypeMemSubmoduleCorootSpanOfFinite Finite.of_fintype range_polarizationIn_le_span_coroot Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap Module.IsTorsionFree.trans_faithfulSMul IsDomain.toIsCancelMulZero Module.IsReflexive.to_isTorsionFree Finset.prod_ne_zero_iff IsDomain.to_noZeroDivisors FaithfulSMul.algebraMap_eq_zero_iff IsAnisotropic.rootForm_root_ne_zero algebraMap_rootFormIn LinearMap.finrank_le_of_isSMulRegular IsScalarTower.left Module.Finite.range instFiniteSubtypeMemSubmoduleRootSpanOfFinite smul_right_injective Submodule.mem_span_range_iff_exists_fun Finset.smul_sum Finset.sum_congr smul_smul mul_comm Submodule.sum_smul_mem prod_rootFormIn_smul_coroot_mem_range_PolarizationIn
finrank_rootSpan_map_polarization_eq_finrank_corootSpan 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Polarization rootSpan Submodule.addCommMonoid Submodule.module corootSpan	—	RingHomSurjective.ids Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial IsScalarTower.left instIsValuedIn finrank_range_polarization_eq_finrank_span_coroot instFaithfulSMul range_polarizationIn
instIsAnisotropicFlip 📖	mathematical	—	IsAnisotropic flip	—	IsAnisotropic.corootForm_coroot_ne_zero IsAnisotropic.rootForm_root_ne_zero
instIsAnisotropicOfIsCrystallographic 📖	mathematical	—	IsAnisotropic	—	isAnisotropic_of_isValuedIn Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero
instIsAnisotropicOfLinearOrderedCommRing 📖	mathematical	—	IsAnisotropic	—	isAnisotropic_of_isValuedIn Module.Free.instFaithfulSMulOfNontrivial Module.Free.self instNontrivialOfCharZero IsStrictOrderedRing.toCharZero instIsValuedIn
instIsBalanced 📖	mathematical	—	IsBalanced EuclideanDomain.toCommRing Field.toEuclideanDomain	—	isPerfPair_toLinearMap Algebra.to_smulCommClass RingHomSurjective.ids RingHomInvPair.ids ker_rootForm_eq_dualAnnihilator isCompl_rootSpan_ker_rootForm ker_corootForm_eq_dualAnnihilator isCompl_corootSpan_ker_corootForm
isAnisotropic_of_isValuedIn 📖	mathematical	—	IsAnisotropic	—	RootPositiveForm.form_apply_root_ne_zero instIsValuedInFlip
isCompl_corootSpan_ker_corootForm 📖	mathematical	—	IsCompl Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice corootSpan LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module CorootForm	—	isCompl_rootSpan_ker_rootForm instIsAnisotropicFlip
isCompl_rootSpan_ker_rootForm 📖	mathematical	—	IsCompl Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice rootSpan LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module RootForm	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap Submodule.isCompl_iff_disjoint Module.instFiniteDimensionalOfIsReflexive smulCommClass_self Algebra.to_smulCommClass LinearEquiv.finrank_eq finrank_corootSpan_eq' instIsDomain Subspace.finrank_add_finrank_dualAnnihilator_eq Subspace.dual_finrank_eq add_le_add_iff_left IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le RingHomSurjective.ids RingHomInvPair.ids LinearEquiv.finrank_map_eq Submodule.finrank_mono commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing FiniteDimensional.finiteDimensional_submodule corootSpan_dualAnnihilator_le_ker_rootForm disjoint_rootSpan_ker_rootForm
ker_corootForm_eq_dualAnnihilator 📖	mathematical	—	LinearMap.ker LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module CorootForm Submodule.map Module.Dual Algebra.to_smulCommClass Algebra.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm LinearMap.toPerfPair toLinearMap flip isPerfPair_toLinearMap Submodule.dualAnnihilator Semifield.toCommSemiring Field.toSemifield rootSpan	—	ker_rootForm_eq_dualAnnihilator instIsAnisotropicFlip
ker_rootForm_eq_dualAnnihilator 📖	mathematical	—	LinearMap.ker LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module RootForm Submodule.map Module.Dual Algebra.to_smulCommClass Algebra.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm LinearMap.toPerfPair toLinearMap isPerfPair_toLinearMap Submodule.dualAnnihilator Semifield.toCommSemiring Field.toSemifield corootSpan	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap smulCommClass_self Subspace.finrank_add_finrank_dualAnnihilator_eq Module.instFiniteDimensionalOfIsReflexive Submodule.finrank_add_eq_of_isCompl isCompl_rootSpan_ker_rootForm Algebra.to_smulCommClass Subspace.dual_finrank_eq LinearEquiv.finrank_eq finrank_corootSpan_eq' instIsDomain RingHomSurjective.ids RingHomInvPair.ids Submodule.eq_of_le_of_finrank_eq FiniteDimensional.finiteDimensional_submodule corootSpan_dualAnnihilator_le_ker_rootForm LinearEquiv.finrank_map_eq
linearIndepOn_coroot_iff 📖	mathematical	—	LinearIndepOn DFunLike.coe Function.Embedding Function.instFunLikeEmbedding coroot EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid root	—	Nat.instAtLeastTwoHAddOfNat instIsAnisotropicFlip instIsRootSystemFlip
orthogonal_corootSpan_eq 📖	mathematical	—	LinearMap.BilinForm.orthogonal CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid CorootForm corootSpan LinearMap.ker LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	orthogonal_rootSpan_eq instIsAnisotropicFlip
orthogonal_rootSpan_eq 📖	mathematical	—	LinearMap.BilinForm.orthogonal CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid RootForm rootSpan LinearMap.ker LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module	—	LinearMap.BilinForm.orthogonal_top_eq_ker LinearMap.IsSymm.isRefl rootForm_symmetric le_antisymm Submodule.mem_sup IsCompl.sup_eq_top isCompl_rootSpan_ker_rootForm Submodule.mem_top map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass add_zero
polarizationEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv PolarizationEquiv LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain LinearMap.instFunLike Polarization	—	RingHomInvPair.ids polarizationEquiv_toLinearMap
polarizationEquiv_symm_apply_coroot 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm PolarizationEquiv Function.Embedding Function.instFunLikeEmbedding coroot EuclideanDomain.toCommRing Field.toEuclideanDomain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Nat.instAtLeastTwoHAddOfNat LinearMap CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm root	—	RingHomInvPair.ids Nat.instAtLeastTwoHAddOfNat coroot_eq_polarizationEquiv_apply_root map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.symm_apply_apply
polarizationEquiv_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid PolarizationEquiv Polarization EuclideanDomain.toCommRing Field.toEuclideanDomain	—	RingHomInvPair.ids Module.instFiniteDimensionalOfIsReflexive Subspace.instModuleDualFiniteDimensional Algebra.to_smulCommClass RingHomCompTriple.ids flip_comp_polarization_eq_rootForm SMulCommClass.symm LinearEquiv.trans.congr_simp LinearMap.linearEquivOfInjective.congr_simp LinearMap.ext isPerfPair_toLinearMap Polarization_apply Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearEquiv.symm_apply_apply
polarizationIn_Injective 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike PolarizationIn	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap Module.IsTorsionFree.trans_faithfulSMul IsDomain.toNontrivial IsDomain.toIsCancelMulZero Module.IsReflexive.to_isTorsionFree LinearMap.ker_eq_bot top_disjoint Submodule.disjoint_ker_of_finrank_le IsDomain.hasRankNullity commRing_strongRankCondition Ideal.instIsTorsionFreeSubtypeMemSubmodule Module.Finite.top instFiniteSubtypeMemSubmoduleRootSpanOfFinite Finite.of_fintype RingHomSurjective.ids finrank_top finrank_corootSpan_eq finrank_range_polarization_eq_finrank_span_coroot Submodule.finrank_mono Module.Finite.map le_of_eq LinearMap.range_eq_map
posRootForm_posForm_anisotropic 📖	mathematical	—	QuadraticMap.Anisotropic Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.module Semiring.toModule LinearMap.BilinMap.toQuadraticMap RootPositiveForm.posForm posRootForm	—	ne_of_lt posRootForm_posForm_pos_of_ne_zero
posRootForm_posForm_nondegenerate 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Submodule.addCommMonoid Submodule.module RootPositiveForm.posForm posRootForm	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq LT.lt.ne' posRootForm_posForm_pos_of_ne_zero
posRootForm_posForm_pos_of_ne_zero 📖	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 root Submodule.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.module Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPositiveForm.posForm posRootForm	—	posRootForm_posForm_apply_apply isAnisotropic_of_isValuedIn exists_coroot_ne IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE Finset.mem_univ mul_self_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing contravariant_lt_of_covariant_le Finset.sum_pos' IsStrictOrderedRing.toIsOrderedCancelAddMonoid mul_self_nonneg IsOrderedRing.toPosMulMono
posRootForm_rootFormIn_posDef 📖	mathematical	—	QuadraticMap.PosDef Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Submodule.addCommMonoid Submodule.module SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule LinearMap.BilinMap.toQuadraticMap RootFormIn	—	posRootForm_eq posRootForm_posForm_pos_of_ne_zero
rootForm_anisotropic 📖	mathematical	—	QuadraticMap.Anisotropic CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule LinearMap.BilinMap.toQuadraticMap RootForm	—	eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero IsRootSystem.span_root_eq_top
rootForm_nondegenerate 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RootForm	—	smulCommClass_self LinearMap.IsRefl.nondegenerate_iff_separatingLeft LinearMap.IsSymm.isRefl rootForm_symmetric IsRootSystem.span_root_eq_top disjoint_rootSpan_ker_rootForm
rootForm_pos_of_ne_zero 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan	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 RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm	—	LE.le.lt_of_ne zero_le_rootForm Mathlib.Tactic.Contrapose.contrapose₄ eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero
rootForm_restrict_nondegenerate_of_isAnisotropic 📖	mathematical	—	LinearMap.Nondegenerate Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan Semifield.toCommSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.addCommMonoid Submodule.module RingHom.id LinearMap.BilinForm.restrict RootForm	—	LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker rootForm_symmetric isCompl_rootSpan_ker_rootForm
rootForm_restrict_nondegenerate_of_ordered 📖	mathematical	—	LinearMap.Nondegenerate Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike rootSpan NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.addCommMonoid Submodule.module RingHom.id LinearMap.BilinForm.restrict RootForm	—	LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker zero_le_rootForm rootForm_symmetric disjoint_rootSpan_ker_rootForm IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE instIsAnisotropicOfLinearOrderedCommRing
rootForm_self_eq_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 RootForm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule SetLike.instMembership Submodule.setLike LinearMap.ker	—	LinearMap.BilinForm.apply_apply_same_eq_zero_iff zero_le_rootForm rootForm_symmetric
rootSpan_eq_top_iff 📖	mathematical	—	rootSpan EuclideanDomain.toCommRing Field.toEuclideanDomain Top.top Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instTop corootSpan	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap Submodule.eq_top_of_finrank_eq Module.instFiniteDimensionalOfIsReflexive finrank_corootSpan_eq' instIsDomain finrank_top Algebra.to_smulCommClass LinearEquiv.finrank_eq Subspace.dual_finrank_eq
smul_coroot_eq_of_root_add_root_eq 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid 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 DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul pairing coroot	—	rootForm_self_smul_coroot smul_assoc IsScalarTower.left SMulCommClass.smul_comm AddMonoid.nat_smulCommClass' map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass nsmul_add map_add SemilinearMapClass.toAddHomClass Nat.instAtLeastTwoHAddOfNat LinearMap.IsSymm.eq rootForm_symmetric Algebra.to_smulCommClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr 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 Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one InvariantForm.two_mul_apply_root_root InvariantForm.pairing_mul_eq_pairing_mul_swap Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₂ zero_add Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero add_smul smul_add smul_right_injective IsDomain.toIsCancelMulZero IsAnisotropic.rootForm_root_ne_zero Mathlib.Tactic.Module.NF.add_eq_eval₁
toInvariantForm_form 📖	mathematical	—	InvariantForm.form toInvariantForm RootForm	—	—
zero_le_rootForm 📖	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 AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootForm	—	IsSumSq.nonneg AddGroup.existsAddOfLE rootForm_self_sum_of_squares

RootPairing.IsAnisotropic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
corootForm_coroot_ne_zero 📖	—	—	—	—	—
rootForm_root_ne_zero 📖	—	—	—	—	—

RootSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rootForm_anisotropic 📖	mathematical	—	QuadraticMap.Anisotropic CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule LinearMap.BilinMap.toQuadraticMap RootPairing.RootForm	—	RootPairing.rootForm_anisotropic
rootForm_nondegenerate 📖	mathematical	—	LinearMap.BilinForm.Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RootPairing.RootForm	—	RootPairing.rootForm_nondegenerate

---

← Back to Index