prime_iff — Mathlib

English

If e is a multiplicative equivalence between M and N, then an element p is prime in M iff e(p) is prime in N.

Русский

Если e — мультипликативное эквивалентство между M и N, то элемент p прост в M тогда и только тогда, когда e(p) прост в N.

LaTeX

$$$\\forall p:\\, M,\\; \\operatorname{Prime}(p) \\iff \\operatorname{Prime}(e(p)).$$$

Lean4

theorem prime_iff {E : Type*} [EquivLike E M N] [MulEquivClass E M N] (e : E) : Prime (e p) ↔ Prime p :=
  by
  let e := MulEquivClass.toMulEquiv e
  exact
    ⟨comap_prime e e.symm fun a => by simp, fun h =>
      (comap_prime e.symm e fun a => by simp) <| (e.symm_apply_apply p).substr h⟩

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