map_mk_comap_factorPow — Mathlib

English

The map equality (I.map (mk I^a)).comap (factorPow I le) = I.map (mk I^b) holds for a ≤ b with a > 0 and le: a ≤ b.

Русский

Справедливость отображений (I.map (mk I^a)).comap (factorPow I le) = I.map (mk I^b) держится при a ≤ b и a > 0.

LaTeX

$$$(I.map (mk (I^a))).comap (factorPow I le) = I.map (mk (I^b))$ при $apos>0$ и $a\le b$.$$

Lean4

theorem map_mk_comap_factorPow {a b : ℕ} (apos : 0 < a) (le : a ≤ b) :
    (I.map (mk (I ^ a))).comap (factorPow I le) = I.map (mk (I ^ b)) :=
  by
  apply Ideal.map_mk_comap_factor
  exact pow_le_self (Nat.ne_zero_of_lt apos)

Похожие утверждения