Structures · Algebra
IsReduced
A structure that has zero and pow is reduced if it has no nonzero nilpotent elements.
- Defined in
- Mathlib.Algebra.GroupWithZero.Basic
- Shape
- One type argument · adds eq_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances8
- ZMod
- CommRingCat.carrier
- TensorProduct
- Localization
- PerfectClosure
- MvPolynomial
- Prod
- Submodule
How is a type an instance?
Loading the hierarchy index…
Assumed by83
- pow_ne_zero
- eq_zero_of_pow_eq_zero
- pow_eq_zero_iff
- IsNilpotent.eq_zero
- sq_eq_zero_iff
- isNilpotent_iff_eq_zero
- IsArtinianRing.equivPi
- isReduced_of_injective
- pow_eq_zero_iff'
- frobenius_inj
- IsReduced.eq_zero
- Ideal.isRadical_bot
- iterateFrobenius_inj
- pow_ne_zero_iff
- nilradical_eq_zero
- not_isPrimePow_zero
- IsPurelyInseparable.injective_comp_algebraMap
- MvPolynomial.isUnit_iff_totalDegree_of_isReduced
- PerfectRing.ofSurjective
- minpoly.isRadical
- Ring.KrullDimLE.isField_of_isReduced
- IsAlgebraic.iff_exists_smul_integral
- Polynomial.not_isUnit_of_natDegree_pos_of_isReduced
- AlgebraicGeometry.isReduced_of_isReduced_stalk
- isStronglyTranscendental_mk_of_mem_minimalPrimes
- Matrix.isParabolic_iff_of_upperTriangular
- isSquare_of_charTwo'
- IsPurelyInseparable.injective_restrictDomain
- PrimeSpectrum.subsingleton_iff_isField_of_isReduced
- pow_pos_iff
- mem_rootsOfUnity_prime_pow_mul_iff
- LieModule.traceForm_eq_zero_of_isNilpotent
- CanonicallyOrderedAdd.pow_pos
- IsPrimePow.ne_zero
- Function.support_pow
- IsArtinianRing.isSemisimpleRing_of_isReduced
- MonomialOrder.degree_pow
- Submodule.pow_eq_bot
- Ideal.radical_bot_of_isReduced
- LinearMap.trace_comp_eq_mul_of_commute_of_isNilpotent
- IsArtinianRing.isField_of_isReduced_of_isLocalRing
- Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAt
- PerfectClosure.instNontrivialOfIsReduced
- Ideal.radical_bot_of_noZeroDivisors
- PerfectRing.ofFiniteOfIsReduced
- IsReduced.pow_eq_zero
- IsReduced.pow_ne_zero
- PerfectClosure.eq_iff
- WeierstrassCurve.addSubMap_ne_zero
- Algebra.not_isStronglyTranscendental_of_quasiFiniteAt
Ancestors0
No ancestors.