Morse

📁 Source: Mathlib/RingTheory/Polynomial/Morse.lean

Statistics

Metric	Count
Definitions	0
Theorems surjective_toPermHom_of_iSup_inertia_eq_top, toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia	2
Total	2

Polynomial.Splits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective_toPermHom_of_iSup_inertia_eq_top 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map algebraMap Set.ncard Polynomial.rootSet HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 MaximalSpectrum.asIdeal Ideal.Quotient.commRing Ideal.Quotient.isDomain CommRing.toRing Ideal.instIsTwoSided_1 Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal Ideal.instAlgebraQuotient iSup Subgroup MaximalSpectrum ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Ideal.inertia DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Top.top Subgroup.instTop	Equiv.Perm Set.Elem DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Equiv.Perm.permGroup MonoidHom.instFunLike MulAction.toPermHom Polynomial.instMulActionElemRootSetOfSMulCommClass	—	Ideal.Quotient.isDomain Ideal.instIsTwoSided_1 Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal surjective_of_isSwap_of_isPretransitive' Finite.of_fintype Set.mem_iUnion toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia Subgroup.closure_iUnion Subgroup.closure_eq
toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map algebraMap Set.ncard Polynomial.rootSet HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.Quotient.commRing Ideal.Quotient.isDomain CommRing.toRing Ideal.instIsTwoSided_1 Ideal.instAlgebraQuotient Subgroup SetLike.instMembership Subgroup.instSetLike Ideal.inertia DistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction	DFunLike.coe MonoidHom Equiv.Perm Set.Elem MulOneClass.toMulOne Monoid.toMulOneClass Equiv.Perm.permGroup MonoidHom.instFunLike MulAction.toPermHom Polynomial.instMulActionElemRootSetOfSMulCommClass Equiv.Perm.instOne Equiv.Perm.IsSwap	—	Ideal.Quotient.isDomain Ideal.instIsTwoSided_1 Equiv.equiv_subsingleton_dom Set.subsingleton_coe Set.ncard_le_one_iff_subsingleton Finite.of_fintype zero_add Set.ncard_empty Finset.coe_empty Multiset.toFinset_zero Polynomial.roots_zero Polynomial.aroots_def Polynomial.rootSet_def Ideal.Quotient.mk_eq_mk_iff_sub_mem Equiv.ext_iff Equiv.Perm.ext Set.ncard_le_ncard_image_add_one_iff image_rootSet_of_map_ne_zero

---

← Back to Index