Theorems · Theorem · commutative algebra
Ideal.span_singleton_pow
∀ {R : Type u} [inst : Semiring R] (s : R) [(Ideal.span {s}).IsTwoSided] (n : ℕ),
Ideal.span {s} ^ n = Ideal.span {s ^ n}- Defined in
- Mathlib.RingTheory.Ideal.Operations
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringIdeal.IsTwoSided
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Moduleproof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- Top.topproof · cited by 9,680
- Submoduleproof · cited by 7,192
- Idealstatement · cited by 4,748
- IsScalarTowerproof · cited by 3,896
- zero_addproof · cited by 2,366
- eq_or_neproof · cited by 1,117
- pow_zeroproof · cited by 1,094
- Ideal.spanstatement and proof · cited by 948
- pow_oneproof · cited by 894
Cited by19
Results whose statement or proof uses this declaration.
- Ideal.exists_radical_pow_le_of_fgproof · cited by 4
- Ideal.relNorm_algebraMapproof · cited by 4
- Ideal.emultiplicity_eq_emultiplicity_spanproof · cited by 3
- LaurentSeries.intValuation_le_iff_coeff_lt_eq_zeroproof · cited by 3
- Ideal.exists_pow_le_of_le_radical_of_fgproof · cited by 2
- Valuation.Integers.maximalIdeal_pow_eq_setOfPred_le_v_algebraMap_powproof · cited by 2
- Ideal.count_associates_eqproof · cited by 2
- dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1
- Submodule.isInternal_prime_power_torsion_of_pidproof · cited by 1
- cyclotomic_comp_X_add_one_isEisensteinAtproof · cited by 1
- cyclotomic_prime_pow_comp_X_add_one_isEisensteinAtproof · cited by 1
- mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1