le_comap_pow — Mathlib

English

The inequality between comap powers and comapped powers: comap f K^n ≤ (comap f K)^n for n ∈ N.

Русский

Неравенство между степенями comap и их образами: comap f K^n ≤ (comap f K)^n.

LaTeX

$$comap f K^n ≤ (comap f K)^n$$

Lean4

theorem le_comap_pow (n : ℕ) : K.comap f ^ n ≤ (K ^ n).comap f := by
  induction n with
  | zero =>
    rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
    exact rfl.le
  | succ n n_ih =>
    rw [pow_succ, pow_succ]
    exact (Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)

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