Nilpotent

📁 Source: Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean

Statistics

Metric	Count
Definitions	0
Theorems induction_on, isUnit_mk_pow_iff_isUnit_mk, isUnit_mk_pow_iff_notMem, isRadical_iff_quotient_reduced, isUnit_quotient_mk_iff	5
Total	5

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRadical_iff_quotient_reduced 📖	mathematical	—	IsRadical CommRing.toCommSemiring IsReduced HasQuotient.Quotient Ideal CommSemiring.toSemiring instHasQuotient_1 Submodule.Quotient.instZeroQuotient CommRing.toRing Ring.toAddCommGroup Semiring.toModule Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quotient.semiring	—	instIsTwoSided_1 RingHom.instRingHomClass mk_ker RingHom.ker_isRadical_iff_reduced_of_surjective Quotient.mk_surjective

Ideal.IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_on 📖	—	IsNilpotent Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	—	—	IsScalarTower.right Ideal.instIsTwoSided_1 Nat.strong_induction_on Ideal.zero_eq_bot zero_pow two_ne_zero subsingleton_of_bot_eq_top Ideal.one_eq_top pow_zero pow_one IsScalarTower.left Ideal.pow_le_self pow_mul eq_bot_iff Ideal.pow_le_pow_right Ideal.map_pow RingHom.instRingHomClass Ideal.map_quotient_self

Ideal.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_mk_pow_iff_isUnit_mk 📖	mathematical	—	IsUnit HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	IsScalarTower.right Ideal.instIsTwoSided_1 IsNilpotent.isUnit_quotient_mk_iff RingHom.instRingHomClass Ideal.map_quotient_self IsScalarTower.left Ideal.pow_le_self isUnit_map_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass isLocalHom_equiv RingEquivClass.toMulEquivClass
isUnit_mk_pow_iff_notMem 📖	mathematical	—	IsUnit HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring ring Ideal.instIsTwoSided_1 RingHom.instFunLike SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	IsScalarTower.right Ideal.instIsTwoSided_1 isUnit_iff_ne_zero Iff.not eq_zero_iff_mem

IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_quotient_mk_iff 📖	mathematical	IsNilpotent Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	IsUnit HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.right Ideal.instIsTwoSided_1 Ideal.IsNilpotent.induction_on Ideal.Quotient.mk_surjective map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass IsUnit.mul_val_inv Ideal.mem_bot Ideal.pow_mem_pow Ideal.Quotient.eq Nat.instAtLeastTwoHAddOfNat sub_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Meta.NormNum.instAtLeastTwo 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.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero 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.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid IsUnit.map sup_eq_right

---

← Back to Index