Artinian rings and modules #
A module satisfying these equivalent conditions is said to be an Artinian R-module
if every decreasing chain of submodules is eventually constant, or equivalently,
if the relation < on submodules is well founded.
A ring is said to be left (or right) Artinian if it is Artinian as a left (or right) module over itself, or simply Artinian if it is both left and right Artinian.
Main results #
IsArtinianRing.primeSpectrum_finite,IsArtinianRing.isMaximal_of_isPrime: there are only finitely prime ideals in a commutative Artinian ring, and each of them is maximal.IsArtinianRing.equivPi: a reduced commutative Artinian ringRis isomorphic to a finite product of fields (and therefore is a semisimple ring and a decomposition monoid; moreoverR[X]is also a decomposition monoid).IsArtinian.isSemisimpleModule_iff_jacobson: an Artinian module is semisimple iff its Jacobson radical is zero.instIsSemiprimaryRingOfIsArtinianRing: an Artinian ringRis semiprimary, in particular the Jacobson radical ofRis a nilpotent ideal (IsArtinianRing.isNilpotent_jacobson_bot).
References #
- [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
- [P. Samuel, Algebraic Theory of Numbers][samuel1967]
Tags #
Artinian, artinian, Artinian ring, Artinian module, artinian ring, artinian module
theorem
LinearMap.isArtinian_iff_of_bijective
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_5}
{P : Type u_6}
[Semiring S]
[AddCommMonoid P]
[Module S P]
{σ : R →+* S}
[RingHomSurjective σ]
(l : M →ₛₗ[σ] P)
(hl : Function.Bijective ⇑l)
:
theorem
isArtinian_of_injective
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid P]
[Module R M]
[Module R P]
(f : M →ₗ[R] P)
(h : Function.Injective ⇑f)
[IsArtinian R P]
:
IsArtinian R M
instance
isArtinian_submodule'
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(N : Submodule R M)
:
IsArtinian R ↥N
theorem
isArtinian_of_le
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s t : Submodule R M}
[IsArtinian R ↥t]
(h : s ≤ t)
:
IsArtinian R ↥s
theorem
isArtinian_of_surjective
{R : Type u_1}
(M : Type u_2)
{P : Type u_3}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid P]
[Module R M]
[Module R P]
(f : M →ₗ[R] P)
(hf : Function.Surjective ⇑f)
[IsArtinian R M]
:
IsArtinian R P
theorem
isArtinian_of_surjective_algebraMap
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_5}
[CommSemiring S]
[Algebra S R]
[Module S M]
[IsArtinian R M]
[IsScalarTower S R M]
(H : Function.Surjective ⇑(algebraMap S R))
:
IsArtinian S M
If M is an Artinian R module, and S is an R-algebra with a surjective
algebra map, then M is an Artinian S module.
instance
isArtinian_range
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid P]
[Module R M]
[Module R P]
(f : M →ₗ[R] P)
[IsArtinian R M]
:
IsArtinian R ↥f.range
theorem
isArtinian_of_linearEquiv
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid P]
[Module R M]
[Module R P]
(f : M ≃ₗ[R] P)
[IsArtinian R M]
:
IsArtinian R P
theorem
LinearEquiv.isArtinian_iff
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid P]
[Module R M]
[Module R P]
(f : M ≃ₗ[R] P)
:
theorem
isArtinian_of_finite
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Finite M]
:
IsArtinian R M
theorem
IsArtinian.finite_of_linearIndependent
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Nontrivial R]
[h : IsArtinian R M]
{s : Set M}
(hs : LinearIndependent R Subtype.val)
:
s.Finite
theorem
set_has_minimal_iff_artinian
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.
theorem
IsArtinian.set_has_minimal
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(a : Set (Submodule R M))
(ha : a.Nonempty)
:
theorem
IsArtinian.eventuallyConst_of_isArtinian
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(f : ℕ →o (Submodule R M)ᵒᵈ)
:
theorem
IsArtinian.surjective_of_injective_endomorphism
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(f : M →ₗ[R] M)
(s : Function.Injective ⇑f)
:
Any injective endomorphism of an Artinian module is surjective.
theorem
IsArtinian.bijective_of_injective_endomorphism
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(f : M →ₗ[R] M)
(s : Function.Injective ⇑f)
:
Any injective endomorphism of an Artinian module is bijective.
theorem
IsArtinian.disjoint_partial_infs_eventually_top
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(f : ℕ → Submodule R M)
(h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1))))
:
A sequence f of submodules of an Artinian module,
with the supremum f (n+1) and the infimum of f 0, ..., f n being ⊤,
is eventually ⊤.
theorem
IsArtinian.subsingleton_of_injective
{R : Type u_1}
{P : Type u_3}
{N : Type u_4}
[Semiring R]
[AddCommMonoid P]
[AddCommMonoid N]
[Module R P]
[Module R N]
[IsArtinian R N]
{f : P × N →ₗ[R] N}
(inj : Function.Injective ⇑f)
:
theorem
LinearMap.eventually_iInf_range_pow_eq
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(f : Module.End R M)
:
instance
isArtinian_of_quotient_of_artinian
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
[IsArtinian R M]
:
IsArtinian R (M ⧸ N)
theorem
isArtinian_of_range_eq_ker
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
{N : Type u_4}
[Ring R]
[AddCommGroup M]
[AddCommGroup P]
[AddCommGroup N]
[Module R M]
[Module R P]
[Module R N]
[IsArtinian R M]
[IsArtinian R P]
(f : M →ₗ[R] N)
(g : N →ₗ[R] P)
(h : f.range = g.ker)
:
IsArtinian R N
theorem
isArtinian_iff_submodule_quotient
{R : Type u_1}
{P : Type u_3}
[Ring R]
[AddCommGroup P]
[Module R P]
(S : Submodule R P)
:
instance
isArtinian_prod
{R : Type u_1}
{M : Type u_2}
{P : Type u_3}
[Ring R]
[AddCommGroup M]
[AddCommGroup P]
[Module R M]
[Module R P]
[IsArtinian R M]
[IsArtinian R P]
:
IsArtinian R (M × P)
instance
isArtinian_sup
{R : Type u_1}
{P : Type u_3}
[Ring R]
[AddCommGroup P]
[Module R P]
(M₁ M₂ : Submodule R P)
[IsArtinian R ↥M₁]
[IsArtinian R ↥M₂]
:
IsArtinian R ↥(M₁ ⊔ M₂)
instance
isArtinian_pi
{R : Type u_1}
[Ring R]
{ι : Type u_5}
[Finite ι]
{M : ι → Type u_6}
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), IsArtinian R (M i)]
:
IsArtinian R ((i : ι) → M i)
instance
isArtinian_pi'
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_5}
[Finite ι]
[IsArtinian R M]
:
IsArtinian R (ι → M)
A version of isArtinian_pi for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
prove that ι → ℝ is finite dimensional over ℝ).
instance
isArtinian_finsupp
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_5}
[Finite ι]
[IsArtinian R M]
:
IsArtinian R (ι →₀ M)
instance
isArtinian_iSup
{R : Type u_1}
{P : Type u_3}
[Ring R]
[AddCommGroup P]
[Module R P]
{ι : Type u_5}
[Finite ι]
{M : ι → Submodule R P}
[∀ (i : ι), IsArtinian R ↥(M i)]
:
IsArtinian R ↥(⨆ (i : ι), M i)
theorem
IsArtinian.isSemisimpleModule_iff_jacobson
(R : Type u_1)
(M : Type u_2)
[Ring R]
[AddCommGroup M]
[Module R M]
[IsArtinian R M]
:
theorem
LinearMap.eventually_codisjoint_ker_pow_range_pow
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
[IsArtinian R M]
(f : Module.End R M)
:
∀ᶠ (n : ℕ) in Filter.atTop, Codisjoint (f ^ n).ker (f ^ n).range
For any endomorphism of an Artinian module, any sufficiently high iterate has codisjoint kernel and range.
theorem
LinearMap.eventually_isCompl_ker_pow_range_pow
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
[IsArtinian R M]
[IsNoetherian R M]
(f : Module.End R M)
:
This is the Fitting decomposition of the module M with respect to the endomorphism f.
See also LinearMap.isCompl_iSup_ker_pow_iInf_range_pow for an alternative spelling.
theorem
LinearMap.isCompl_iSup_ker_pow_iInf_range_pow
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
[IsArtinian R M]
[IsNoetherian R M]
(f : M →ₗ[R] M)
:
This is the Fitting decomposition of the module M with respect to the endomorphism f.
See also LinearMap.eventually_isCompl_ker_pow_range_pow for an alternative spelling.
theorem
IsArtinian.range_smul_pow_stabilizes
{R : Type u_1}
(M : Type u_2)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(r : R)
:
theorem
IsArtinian.exists_pow_succ_smul_dvd
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[IsArtinian R M]
(r : R)
(x : M)
:
theorem
isArtinian_of_submodule_of_artinian
(R : Type u_1)
(M : Type u_2)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(N : Submodule R M)
:
IsArtinian R M → IsArtinian R ↥N
theorem
isArtinian_of_tower
(R : Type u_1)
{S : Type u_2}
{M : Type u_3}
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[SMul R S]
[Module S M]
[Module R M]
[IsScalarTower R S M]
(h : IsArtinian R M)
:
IsArtinian S M
If M / S / R is a scalar tower, and M / R is Artinian, then M / S is also Artinian.
instance
instIsArtinianRingQuotientIdeal
(R : Type u_1)
[Ring R]
[IsArtinianRing R]
(I : Ideal R)
[I.IsTwoSided]
:
IsArtinianRing (R ⧸ I)
@[instance 100]
instance
instIsDedekindFiniteMonoidOfIsArtinianRing
(R : Type u_1)
[Semiring R]
[IsArtinianRing R]
:
instance
isArtinian_of_fg_of_artinian'
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
[IsArtinianRing R]
[Module.Finite R M]
:
IsArtinian R M
theorem
isArtinian_of_fg_of_artinian
{R : Type u_1}
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
[IsArtinianRing R]
(hN : N.FG)
:
IsArtinian R ↥N
theorem
IsArtinianRing.of_finite
(R : Type u_1)
(S : Type u_2)
[Ring R]
[Ring S]
[Module R S]
[IsScalarTower R S S]
[IsArtinianRing R]
[Module.Finite R S]
:
instance
instIsNoetherianRingMatrix
(n : Type u_1)
(R : Type u_2)
[Fintype n]
[DecidableEq n]
[Ring R]
[IsNoetherianRing R]
:
IsNoetherianRing (Matrix n n R)
instance
instIsArtinianRingMatrix
(n : Type u_1)
(R : Type u_2)
[Fintype n]
[DecidableEq n]
[Ring R]
[IsArtinianRing R]
:
IsArtinianRing (Matrix n n R)
theorem
isArtinian_span_of_finite
(R : Type u_1)
{M : Type u_2}
[Ring R]
[AddCommGroup M]
[Module R M]
[IsArtinianRing R]
{A : Set M}
(hA : A.Finite)
:
IsArtinian R ↥(Submodule.span R A)
In a module over an Artinian ring, the submodule generated by finitely many vectors is Artinian.
theorem
Function.Surjective.isArtinianRing
{R : Type u_1}
[Semiring R]
{S : Type u_2}
[Semiring S]
{F : Type u_3}
[FunLike F R S]
[RingHomClass F R S]
{f : F}
(hf : Surjective ⇑f)
[H : IsArtinianRing R]
:
instance
isArtinianRing_rangeS
{R : Type u_1}
[Semiring R]
{S : Type u_2}
[Semiring S]
(f : R →+* S)
[IsArtinianRing R]
:
instance
isArtinianRing_range
{R : Type u_1}
[Ring R]
{S : Type u_2}
[Ring S]
(f : R →+* S)
[IsArtinianRing R]
:
theorem
RingEquiv.isArtinianRing
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Semiring S]
(f : R ≃+* S)
[IsArtinianRing R]
:
instance
instIsArtinianRingProd
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Semiring S]
[IsArtinianRing R]
[IsArtinianRing S]
:
IsArtinianRing (R × S)
instance
instIsArtinianRingForallOfFinite
{ι : Type u_2}
[Finite ι]
{R : ι → Type u_1}
[(i : ι) → Semiring (R i)]
[∀ (i : ι), IsArtinianRing (R i)]
:
IsArtinianRing ((i : ι) → R i)
theorem
IsArtinianRing.isUnit_iff_isRightRegular
{R : Type u_1}
[Semiring R]
[IsArtinianRing R]
{x : R}
:
theorem
IsArtinianRing.isUnit_iff_isRegular
{R : Type u_1}
[Semiring R]
[IsArtinianRing R]
{x : R}
:
theorem
IsArtinianRing.isUnit_iff_isLeftRegular
{R : Type u_1}
[Semiring R]
[IsArtinianRing Rᵐᵒᵖ]
{x : R}
:
theorem
IsArtinianRing.isUnit_iff_isRegular_of_mulOpposite
{R : Type u_1}
[Semiring R]
[IsArtinianRing Rᵐᵒᵖ]
{x : R}
:
theorem
IsArtinianRing.isUnit_of_mem_nonZeroDivisors
{R : Type u_1}
[Ring R]
[IsArtinianRing R]
{a : R}
(ha : a ∈ nonZeroDivisors R)
:
IsUnit a
If an element of an Artinian ring is not a zero divisor then it is a unit.
theorem
IsArtinianRing.isUnit_of_mem_nonZeroDivisors_of_mulOpposite
{R : Type u_1}
[Ring R]
[IsArtinianRing Rᵐᵒᵖ]
{a : R}
(ha : a ∈ nonZeroDivisors R)
:
IsUnit a
theorem
IsArtinianRing.isUnit_iff_mem_nonZeroDivisors
{R : Type u_1}
[Ring R]
[IsArtinianRing R]
{a : R}
:
In an Artinian ring, an element is a unit iff it is a non-zero-divisor.
See also isUnit_iff_mem_nonZeroDivisors_of_finite.
theorem
IsArtinianRing.isUnit_iff_mem_nonZeroDivisors_of_mulOpposite
{R : Type u_1}
[Ring R]
[IsArtinianRing Rᵐᵒᵖ]
{a : R}
:
theorem
IsArtinianRing.isUnitSubmonoid_eq_of_mulOpposite
(R : Type u_1)
[Ring R]
[IsArtinianRing Rᵐᵒᵖ]
:
theorem
IsArtinianRing.isUnitSubmonoid_eq_nonZeroDivisorsRight
(R : Type u_1)
[Ring R]
[IsArtinianRing R]
:
theorem
IsArtinianRing.nonZeroDivisorsLeft_eq_isUnitSubmonoid
(R : Type u_1)
[Ring R]
[IsArtinianRing Rᵐᵒᵖ]
:
instance
IsArtinianRing.instFiniteMaximalSpectrum
(R : Type u_1)
[CommSemiring R]
[IsArtinianRing R]
:
theorem
IsArtinianRing.isField_of_isDomain
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
[IsDomain R]
:
IsField R
instance
IsArtinianRing.isMaximal_of_isPrime
{R : Type u_2}
[CommRing R]
(p : Ideal R)
[p.IsPrime]
[IsArtinianRing R]
:
theorem
IsArtinianRing.isPrime_iff_isMaximal
{R : Type u_1}
[CommRing R]
[IsArtinianRing R]
(p : Ideal R)
:
theorem
IsArtinianRing.mem_minimalPrimes
{R : Type u_1}
[CommRing R]
[IsArtinianRing R]
{I p : Ideal R}
[hp : p.IsPrime]
(hIp : I ≤ p)
:
def
IsArtinianRing.primeSpectrumEquivMaximalSpectrum
{R : Type u_1}
[CommRing R]
[IsArtinianRing R]
:
The prime spectrum is in bijection with the maximal spectrum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal
{R : Type u_1}
[CommRing R]
[IsArtinianRing R]
(I : PrimeSpectrum R)
:
@[simp]
theorem
IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal
{R : Type u_1}
[CommRing R]
[IsArtinianRing R]
(I : MaximalSpectrum R)
:
theorem
IsArtinianRing.primeSpectrum_asIdeal_range_eq
{R : Type u_1}
[CommRing R]
[IsArtinianRing R]
:
theorem
IsArtinianRing.nilradical_pow_eq_iInf
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
(n : ℕ)
:
instance
IsArtinianRing.instFinitePrimeSpectrum
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
:
Finite (PrimeSpectrum R)
@[implicit_reducible]
noncomputable def
IsArtinianRing.fieldOfSubtypeIsMaximal
(R : Type u_1)
[CommRing R]
(I : MaximalSpectrum R)
:
A temporary field instance on the quotients by maximal ideals.
Equations
Instances For
noncomputable def
IsArtinianRing.quotNilradicalEquivPi
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
:
The quotient of a commutative Artinian ring by its nilradical is isomorphic to a finite product of fields, namely the quotients by the maximal ideals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IsArtinianRing.quotNilradicalEquivPi_symm_apply
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
(a✝ : (I : MaximalSpectrum R) → R ⧸ I.asIdeal)
:
(quotNilradicalEquivPi R).symm a✝ = (Ideal.quotientEquivAlgOfEq R ⋯).toRingEquiv.symm
({ toEquiv := ↑(Ideal.quotientInfRingEquivPiQuotient MaximalSpectrum.asIdeal ⋯), map_mul' := ⋯, map_add' := ⋯,
commutes' := ⋯ }.toRingEquiv.symm
a✝)
@[simp]
theorem
IsArtinianRing.quotNilradicalEquivPi_apply
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
(a✝ : R ⧸ nilradical R)
(I : MaximalSpectrum R)
:
(quotNilradicalEquivPi R) a✝ I = (Ideal.quotientInfRingEquivPiQuotient MaximalSpectrum.asIdeal ⋯) ((Ideal.quotientEquivAlgOfEq R ⋯) a✝) I
noncomputable def
IsArtinianRing.quotNilradicalPowEquivPi
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
(n : ℕ)
:
The quotient of a commutative Artinian ring by a power of its nilradical is isomorphic to a finite product of local rings, namely the quotients by the powers of the maximal ideals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
IsArtinianRing.quotNilradicalPowEquivPi_symm_apply
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
(n : ℕ)
(a✝ : (I : MaximalSpectrum R) → R ⧸ I.asIdeal ^ n)
:
(quotNilradicalPowEquivPi R n).symm a✝ = (Ideal.quotientEquivAlgOfEq R ⋯).toRingEquiv.symm
({ toEquiv := ↑(Ideal.quotientInfRingEquivPiQuotient (fun (I : MaximalSpectrum R) => I.asIdeal ^ n) ⋯),
map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }.toRingEquiv.symm
a✝)
@[simp]
theorem
IsArtinianRing.quotNilradicalPowEquivPi_apply
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
(n : ℕ)
(a✝ : R ⧸ nilradical R ^ n)
(I : MaximalSpectrum R)
:
(quotNilradicalPowEquivPi R n) a✝ I = (Ideal.quotientInfRingEquivPiQuotient (fun (I : MaximalSpectrum R) => I.asIdeal ^ n) ⋯)
((Ideal.quotientEquivAlgOfEq R ⋯) a✝) I
noncomputable def
IsArtinianRing.equivPi
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
[IsReduced R]
:
A reduced commutative Artinian ring is isomorphic to a finite product of fields, namely the quotients by the maximal ideals.
Equations
Instances For
theorem
IsArtinianRing.isSemisimpleRing_of_isReduced
(R : Type u_1)
[CommRing R]
[IsArtinianRing R]
[IsReduced R]
: