Radical

📁 Source: Mathlib/LinearAlgebra/QuadraticForm/Radical.lean

Statistics

Metric	Count
Definitions radical	1
Theorems finrank_radical_of_equiv_weightedSumSquares, radical_weightedSumSquares, rank_radical_eq, map_radical, radical_eq_bot, rank_rad_polar_le, le_radical_iff, lift_mk, mem_radical_iff', nondegenerate_associated_iff, nondegenerate_iff_radical_eq_bot, nondegenerate_polar_iff, radical_eq_ker_associated, radical_eq_ker_polarBilin, radical_le_ker_polarBilin	15
Total	16

QuadraticForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_radical_of_equiv_weightedSumSquares 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike QuadraticMap.radical Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.addCommMonoid Submodule.module Set.ncard setOf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass QuadraticMap.Equivalent.rank_radical_eq Finite.of_fintype radical_weightedSumSquares Pi.dim_spanSubset IsNoetherianRing.strongRankCondition EuclideanDomain.toNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain
radical_weightedSumSquares 📖	mathematical	—	QuadraticMap.radical Pi.addCommGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule QuadraticMap.weightedSumSquares MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id Pi.spanSubset Finite.of_fintype setOf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instAtLeastTwoHAddOfNat Submodule.ext Algebra.to_smulCommClass Finite.of_fintype QuadraticMap.weightedSumSquares_apply Finset.sum_congr add_sq mul_add Distrib.leftDistribClass Finset.sum_add_distrib AddRightCancelSemigroup.toIsRightCancelAdd Pi.single_apply mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq' zero_add IsDomain.to_noZeroDivisors instIsDomain Finset.sum_eq_zero

QuadraticMap

Definitions

Name	Category	Theorems
radical 📖	CompOp	12 math math: Nondegenerate.radical_eq_bot, le_radical_iff, IsometryEquiv.map_radical, radical_eq_ker_polarBilin, QuadraticForm.sigPos_add_sigNeg_add_radical, Equivalent.rank_radical_eq, QuadraticForm.finrank_radical_of_equiv_weightedSumSquares, radical_eq_ker_associated, QuadraticForm.radical_weightedSumSquares, radical_le_ker_polarBilin, nondegenerate_iff_radical_eq_bot, mem_radical_iff'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_radical_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder radical QuadraticMap HasQuotient.Quotient Submodule.hasQuotient CommRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module comp Submodule.mkQ	—	Submodule.Quotient.mk_eq_zero map_zero zeroHomClass zero_add sub_zero sub_self
lift_mk 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder radical	DFunLike.coe QuadraticMap HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module instFunLike lift	—	—
mem_radical_iff' 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike radical DFunLike.coe QuadraticMap instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	polar_add_left polar_smul_left polar_add_right polar_smul_right sub_sub zero_add
nondegenerate_associated_iff 📖	mathematical	—	LinearMap.Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap QuadraticMap LinearMap.BilinMap instAddCommMonoid LinearMap.addCommMonoid LinearMap.module instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike associated instInvertibleEndOfNat Nondegenerate	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass nondegenerate_iff_radical_eq_bot radical_eq_ker_associated LinearMap.IsRefl.nondegenerate_iff_separatingLeft SMulCommClass.symm IsScalarTower.to_smulCommClass IsScalarTower.left IsScalarTower.to_smulCommClass' associated_flip LinearMap.separatingLeft_iff_ker_eq_bot
nondegenerate_iff_radical_eq_bot 📖	mathematical	—	Nondegenerate radical Bot.bot Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	Nat.instAtLeastTwoHAddOfNat Nondegenerate.radical_eq_bot radical_eq_ker_polarBilin Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton instReflLe rank_subsingleton' Unique.instSubsingleton Cardinal.canonicallyOrderedAdd
nondegenerate_polar_iff 📖	mathematical	—	LinearMap.Nondegenerate CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring polarBilin Nondegenerate	—	Nat.instAtLeastTwoHAddOfNat nondegenerate_iff_radical_eq_bot radical_eq_ker_polarBilin LinearMap.IsRefl.nondegenerate_iff_separatingLeft polar_comm smulCommClass_self LinearMap.separatingLeft_iff_ker_eq_bot
radical_eq_ker_associated 📖	mathematical	—	radical LinearMap.ker LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module DFunLike.coe QuadraticMap LinearMap.BilinMap instAddCommMonoid instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike associated instInvertibleEndOfNat	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass radical_eq_ker_polarBilin Submodule.ext smul_zero
radical_eq_ker_polarBilin 📖	mathematical	—	radical LinearMap.ker LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module polarBilin	—	Nat.instAtLeastTwoHAddOfNat Submodule.ext sub_zero sub_self add_sub_cancel_right two_smul IsUnit.smul_eq_zero isUnit_of_invertible smul_sub SemigroupAction.mul_smul sub_sub map_smul
radical_le_ker_polarBilin 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder radical LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module polarBilin	—	sub_zero sub_self

QuadraticMap.Equivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_radical_eq 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike QuadraticMap.radical Submodule.addCommMonoid Submodule.module	—	RingHomSurjective.ids RingHomInvPair.ids QuadraticMap.IsometryEquiv.map_radical LinearEquiv.finrank_map_eq

QuadraticMap.IsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_radical 📖	mathematical	—	Submodule.map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids toLinearEquiv QuadraticMap.radical	—	Submodule.ext RingHomSurjective.ids RingHomInvPair.ids RingHomSurjective.invPair map_app apply_symm_apply map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass instLinearEquivClass Equiv.forall_congr_left

QuadraticMap.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
radical_eq_bot 📖	mathematical	QuadraticMap.Nondegenerate	QuadraticMap.radical Bot.bot Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	—
rank_rad_polar_le 📖	mathematical	QuadraticMap.Nondegenerate	Cardinal Cardinal.instLE Module.rank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module QuadraticMap.polarBilin Submodule.addCommMonoid Submodule.module Cardinal.instOne	—	—

---

← Back to Index