irreducible_iff — Mathlib

English

If f is a multiplicative equivalence between M and N, then an element x ∈ M is irreducible iff its image f(x) ∈ N is irreducible.

Русский

Если f — мультипликативное эквивалентное отображение между M и N, то элемент x ∈ M неразложим тогда и только тогда, когда его образ f(x) ∈ N неразложим.

LaTeX

$$$\\\\forall {F M N} [Monoid M] [Monoid N] [EquivLike F M N] [MulEquivClass F M N] (f : F), \\\\Irreducible (EquivLike.toFunLike.coe f x) \\\\Leftrightarrow \\\\Irreducible x$$$

Lean4

@[to_additive]
theorem irreducible_iff : Irreducible (f x) ↔ Irreducible x := by
  simp [_root_.irreducible_iff, (EquivLike.surjective f).forall, ← map_mul, -isUnit_map_iff]

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