smul — Mathlib

English

The action of a group on ideals preserves primality: if I is prime, then g • I is prime for any g ∈ M.

Русский

Действие группы на идеалы сохраняет простоту: если I прост, то g • I прост для любого g ∈ M.

LaTeX

$$$\forall I \in \text{Ideal}(R)\, \forall g \in M:\ (g \cdot I).IsPrime$$$

Lean4

instance smul {I : Ideal R} [H : I.IsPrime] (g : M) : (g • I).IsPrime :=
  by
  rw [I.pointwise_smul_eq_comap]
  apply H.comap

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