Basic

📁 Source: Mathlib/RingTheory/Invariant/Basic.lean

Statistics

Metric	Count
Definitions stabilizerQuotientInertiaEquiv, stabilizerHom, MulSemiringAction, charpoly, instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra, instMulSemiringActionQuotientSubgroupSubtypeMemSubringSubring	6
Theorems charpoly_mem_lifts, exists_smul_of_under_eq, isIntegral, orbit_eq_primesOver, isInvariant_of_isGalois, isInvariant_of_isGalois', exists_algEquiv_fixedPoint_quotient_under, exists_algHom_fixedPoint_quotient_under, finite_of_isInvariant, normal, stabilizerHom_surjective, stabilizerQuotientInertiaEquiv_mk, stabilizerHom_surjective, charpoly_eq, charpoly_eq_prod_smul, eval_charpoly, monic_charpoly, smul_charpoly, smul_coeff_charpoly, instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra, instSMulDistribClassAlgEquiv	22
Total	28

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInvariant_of_isGalois 📖	mathematical	—	IsInvariant AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.aut IsIntegralClosure.MulSemiringAction IsSeparable.isAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing IsLocalRing.toNontrivial Field.instIsLocalRing IsGalois.to_isSeparable	—	List.TFAE.out IsGalois.tfae IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing IsGalois.to_isSeparable algebraMap_galRestrict_apply IntermediateField.mem_bot IsIntegralClosure.isIntegral IsIntegrallyClosed.algebraMap_eq_of_integral isIntegral_algebraMap_iff FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsFractionRing.instFaithfulSMul IsScalarTower.algebraMap_apply
isInvariant_of_isGalois' 📖	mathematical	—	IsInvariant AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv.aut AlgEquiv.applyMulSemiringAction	—	IsInvariant.isInvariant IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing IsGalois.to_isSeparable isInvariant_of_isGalois

Algebra.IsInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_mem_lifts 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Subsemiring Semiring.toNonAssocSemiring Polynomial.semiring SetLike.instMembership Subsemiring.instSetLike Polynomial.lifts algebraMap MulSemiringAction.charpoly	—	Polynomial.lifts_iff_coeff_lifts isInvariant MulSemiringAction.smul_coeff_charpoly
exists_smul_of_under_eq 📖	mathematical	Ideal.under CommRing.toCommSemiring CommSemiring.toSemiring	Ideal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Ideal.pointwiseDistribMulAction	—	nonempty_fintype Ideal.subset_union_prime Ideal.IsPrime.smul isInvariant Finset.smul_prod_perm Ideal.IsPrime.prod_mem_iff RingHom.instRingHomClass Ideal.mem_comap Ideal.under_def Finset.mem_univ one_smul Set.mem_biUnion Ideal.mem_inv_pointwise_smul_iff Ideal.under_smul le_antisymm smul_eq_of_le_smul Ideal.instCovariantClassHSMulLe LE.le.trans
isIntegral 📖	mathematical	—	Algebra.IsIntegral CommRing.toRing	—	nonempty_fintype Polynomial.lifts_and_natDegree_eq_and_monic charpoly_mem_lifts MulSemiringAction.monic_charpoly Polynomial.eval_map MulSemiringAction.eval_charpoly
orbit_eq_primesOver 📖	mathematical	—	MulAction.orbit Ideal CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid Ideal.pointwiseDistribMulAction Ideal.primesOver	—	Set.ext Ideal.IsPrime.smul Ideal.LiesOver.smul exists_smul_of_under_eq Ideal.LiesOver.over

Ideal.Quotient

Definitions

Name	Category	Theorems
stabilizerQuotientInertiaEquiv 📖	CompOp	1 math math: stabilizerQuotientInertiaEquiv_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_algEquiv_fixedPoint_quotient_under 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Semiring.toNonAssocSemiring commSemiring RingHom.instFunLike algebraMap AlgEquiv semiring algebraOfLiesOver AlgEquiv.instFunLike	—	FaithfulSMul.algebraMap_injective exists_algHom_fixedPoint_quotient_under Ideal.instIsTwoSided_1 mk_surjective AlgEquiv.symm_apply_apply AlgEquiv.apply_symm_apply MonoidHom.map_mul' RingHom.map_add' AlgHom.commutes'
exists_algHom_fixedPoint_quotient_under 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Semiring.toNonAssocSemiring commSemiring RingHom.instFunLike algebraMap AlgHom semiring algebraOfLiesOver AlgHom.funLike	—	FaithfulSMul.algebraMap_injective Ideal.instIsTwoSided_1 mk_surjective nonempty_fintype IsScalarTower.of_algebraMap_eq' Algebra.IsInvariant.charpoly_mem_lifts Polynomial.aeval_def Polynomial.eval_map Polynomial.coe_mapRingHom MulSemiringAction.eval_charpoly IsScalarTower.of_algebraMap_eq IsScalarTower.algebraMap_apply DFunLike.congr_fun Polynomial.aeval_algHom AlgHom.comp_apply algebraMap_eq Polynomial.aeval_algebraMap_apply isScalarTower IsScalarTower.right map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_prod MonoidWithZeroHomClass.toMonoidHomClass Finset.prod_congr Polynomial.aeval_sub Polynomial.aeval_X Polynomial.aeval_C IsDomain.toNontrivial IsDomain.to_noZeroDivisors Polynomial.aeval_map_algebraMap AlgEquiv.apply_symm_apply
finite_of_isInvariant 📖	mathematical	—	Module.Finite HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule commSemiring algebraOfLiesOver	—	normal Finite.of_surjective Subgroup.instFiniteSubtypeMem stabilizerHom_surjective Ideal.IsMaximal.isPrime' IsGalois.finiteDimensional_of_finite
normal 📖	mathematical	—	Normal HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 field algebraOfLiesOver	—	subsingleton_or_nontrivial Ideal.IsMaximal.ne_top Unique.instSubsingleton Algebra.IsInvariant.isIntegral Algebra.IsIntegral.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing algebra_isIntegral_of_liesOver Ideal.instIsTwoSided_1 mk_surjective nonempty_fintype Polynomial.lifts_and_degree_eq_and_monic Algebra.IsInvariant.charpoly_mem_lifts MulSemiringAction.monic_charpoly Polynomial.aeval_def Polynomial.eval_map MulSemiringAction.eval_charpoly minpoly.dvd Polynomial.aeval_map_algebraMap isScalarTower_of_liesOver IsScalarTower.left Polynomial.aeval_algebraMap_apply isScalarTower IsScalarTower.right map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.Splits.of_dvd isDomain Ideal.IsMaximal.isPrime' Polynomial.map_map IsScalarTower.algebraMap_eq MulSemiringAction.charpoly_eq Polynomial.map_prod Polynomial.Splits.prod Polynomial.Splits.map Polynomial.Splits.X_sub_C Polynomial.Monic.ne_zero Polynomial.Monic.map Polynomial.map_dvd_map'
stabilizerHom_surjective 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal CommSemiring.toSemiring CommRing.toCommSemiring DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule Ideal.pointwiseDistribMulAction AlgEquiv HasQuotient.Quotient Ideal.instHasQuotient_1 commSemiring semiring algebraOfLiesOver DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Subgroup.toGroup AlgEquiv.aut MonoidHom.instFunLike stabilizerHom	—	Ideal.IsPrime.under Ideal.over_def isDomain Ideal.instIsTwoSided_1 FractionRing.instFaithfulSMul instFaithfulSMul OreLocalization.instIsScalarTower IsScalarTower.right FractionRing.instIsScalarTower IsScalarTower.left Localization.isLocalization IsFractionRing.stabilizerHom_surjective Function.Surjective.of_comp_left MonoidHom.coe_comp IsFractionRing.stabilizerHom.eq_1 IsFractionRing.fieldEquivOfAlgEquivHom_injective
stabilizerQuotientInertiaEquiv_mk 📖	mathematical	—	DFunLike.coe MulEquiv HasQuotient.Quotient Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal CommSemiring.toSemiring CommRing.toCommSemiring DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule Ideal.pointwiseDistribMulAction Subgroup.toGroup QuotientGroup.instHasQuotientSubgroup Subgroup.subgroupOf Ideal.inertia CommRing.toRing NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction AlgEquiv Ideal.instHasQuotient_1 commSemiring semiring algebraOfLiesOver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass QuotientGroup.Quotient.group Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia AlgEquiv.aut EquivLike.toFunLike MulEquiv.instEquivLike stabilizerQuotientInertiaEquiv MonoidHom MonoidHom.instFunLike stabilizerHom	—	Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia

IsFractionRing

Definitions

Name	Category	Theorems
stabilizerHom 📖	CompOp	1 math math: stabilizerHom_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stabilizerHom_surjective 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike MulAction.stabilizer Ideal CommSemiring.toSemiring CommRing.toCommSemiring DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne Semiring.toModule Ideal.pointwiseDistribMulAction AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Subgroup.toGroup AlgEquiv.aut MonoidHom.instFunLike stabilizerHom	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass FixedPoints.toAlgAut_surjective Subgroup.instFiniteSubtypeMem AlgEquiv.ext_iff

IsIntegralClosure

Definitions

Name	Category	Theorems
MulSemiringAction 📖	CompOp	2 math math: Algebra.isInvariant_of_isGalois, instSMulDistribClassAlgEquiv

MulSemiringAction

Definitions

Name	Category	Theorems
charpoly 📖	CompOp	7 math math: charpoly_eq_prod_smul, smul_coeff_charpoly, smul_charpoly, eval_charpoly, charpoly_eq, monic_charpoly, Algebra.IsInvariant.charpoly_mem_lifts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_eq 📖	mathematical	—	charpoly Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing Finset.univ Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid toDistribMulAction Ring.toSemiring	—	—
charpoly_eq_prod_smul 📖	mathematical	—	charpoly Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing Finset.univ SMulZeroClass.toSMul Polynomial.instZero Polynomial.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid toDistribMulAction Ring.toSemiring Polynomial.instSub Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	Finset.prod_congr smul_sub Polynomial.smul_X Polynomial.smul_C
eval_charpoly 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring charpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	charpoly_eq Polynomial.eval_prod Finset.prod_eq_zero Finset.mem_univ one_smul Polynomial.eval_sub Polynomial.eval_C Polynomial.eval_X sub_self
monic_charpoly 📖	mathematical	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring charpoly	—	Polynomial.monic_prod_of_monic Polynomial.monic_X_sub_C
smul_charpoly 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul Polynomial.instZero Polynomial.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid toDistribMulAction Ring.toSemiring charpoly	—	charpoly_eq_prod_smul Finset.smul_prod_perm
smul_coeff_charpoly 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid toDistribMulAction Ring.toSemiring Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring charpoly	—	Polynomial.coeff_smul smul_charpoly

(root)

Definitions

Name	Category	Theorems
instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra 📖	CompOp	2 math math: instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient, instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra
instMulSemiringActionQuotientSubgroupSubtypeMemSubringSubring 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient 📖	mathematical	—	Algebra.IsInvariant Subalgebra CommRing.toCommSemiring Ring.toSemiring CommRing.toRing SetLike.instMembership Subalgebra.instSetLike FixedPoints.subalgebra Subgroup Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul HasQuotient.Quotient QuotientGroup.instHasQuotientSubgroup Subalgebra.toSemiring Subalgebra.algebra QuotientGroup.Quotient.group instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra	—	Subgroup.smulCommClass_left Algebra.IsInvariant.isInvariant
instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra 📖	mathematical	—	SMulCommClass HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subalgebra CommRing.toCommSemiring Ring.toSemiring CommRing.toRing SetLike.instMembership Subalgebra.instSetLike FixedPoints.subalgebra Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.mulSemiringAction Subgroup.smulCommClass_left DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring MulSemiringAction.toDistribMulAction Algebra.toSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subalgebra.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul QuotientGroup.Quotient.group Subalgebra.toSemiring instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra Subalgebra.algebra	—	Subgroup.smulCommClass_left SMulCommClass.smul_comm
instSMulDistribClassAlgEquiv 📖	mathematical	—	AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut MulSemiringAction.toDistribMulAction Ring.toSemiring IsIntegralClosure.MulSemiringAction MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero instSMulZeroClass MulSemiringAction.toMulDistribMulAction AlgEquiv.applyMulSemiringAction Algebra.toSMul CommRing.toCommSemiring	—	Algebra.smul_def smul_mul' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass algebraMap_galRestrictHom_apply

---

← Back to Index