Theorems · Theorem · commutative algebra
Ideal.map_pow
∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
[rc : RingHomClass F R S] (f : F) (I : Ideal R) (n : ℕ), Ideal.map f (I ^ n) = Ideal.map f I ^ n- Defined in
- Mathlib.RingTheory.Ideal.Maps
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Idealstatement and proof · cited by 4,748
- FunLikestatement and proof · cited by 2,560
- Ideal.mapstatement · cited by 692
- map_powproof · cited by 503
- RingHomClassstatement and proof · cited by 193
- Ideal.mapHomproof · cited by 2
Cited by17
Results whose statement or proof uses this declaration.
- Algebra.FormallyUnramified.iff_comp_injective_of_smallproof · cited by 4
- Ideal.relNorm_algebraMapproof · cited by 4
- Ideal.IsNilpotent.induction_onproof · cited by 3
- Ideal.ramificationIdx'_eq_one_of_map_localizationproof · cited by 3
- Ideal.ramificationIdx'_eq_ramificationIdx'proof · cited by 3
- IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotientproof · cited by 2
- Ideal.ramificationIdx'_algebra_towerproof · cited by 2
- Ideal.ramificationIdx'_comap_eqproof · cited by 2
- IsUnramifiedAt.of_liesOver_of_ne_botproof · cited by 1
- Algebra.FormallyUnramified.pi_iffproof · cited by 1
- Ideal.mapCotangent_ker_of_surjectiveproof · cited by 1
- IsLocalization.AtPrime.under_maximalIdeal_powproof · cited by 1