uniqueFactorizationMonoid_iff — Mathlib

English

Equivalence between UFMonoid structures under MulEquiv.

Русский

Эквивалентность структур УФМ под множителем-эквивалентностью.

LaTeX

$$$\text{MulEquiv.uniqueFactorizationMonoid}_1( e ) \Leftrightarrow \text{MulEquiv.uniqueFactorizationMonoid}_2( e )$$$

Lean4

theorem uniqueFactorizationMonoid_iff (e : α ≃* β) : UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β :=
  ⟨e.uniqueFactorizationMonoid, e.symm.uniqueFactorizationMonoid⟩

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