English
Two images under a multiplicative equivalence are irreducible exactly when their preimages are irreducible.
Русский
Образы под мультиэквивалентом сохраняют неразложимость: образ неразложим тогда и только тогда, когда прообраз разложим.
LaTeX
$$$\\\\forall {F M N} [Monoid M] [Monoid N] [EquivLike F M N] [MulEquivClass F M N] (f : F), \\\\Irreducible (instHMul.hMul (inst2.coe f x)) \\\\Leftrightarrow \\\\Irreducible x$$$
Lean4
/-- Define a `Group` structure on a Type by proving `∀ a, 1 * a = a` and
`∀ a, a⁻¹ * a = 1`.
Note that this uses the default definitions for `npow`, `zpow` and `div`.
See note [reducible non-instances]. -/
@[to_additive /-- Define an `AddGroup` structure on a Type by proving `∀ a, 0 + a = a` and
`∀ a, -a + a = 0`.
Note that this uses the default definitions for `nsmul`, `zsmul` and `sub`.
See note [reducible non-instances]. -/
]
abbrev ofLeftAxioms {G : Type u} [Mul G] [Inv G] [One G] (assoc : ∀ a b c : G, (a * b) * c = a * (b * c))
(one_mul : ∀ a : G, 1 * a = a) (inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1) : Group G :=
{ mul_assoc := assoc, one_mul := one_mul, inv_mul_cancel := inv_mul_cancel,
mul_one := fun a =>
by
have mul_inv_cancel : ∀ a : G, a * a⁻¹ = 1 := fun a =>
calc
a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
_ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by rw [inv_mul_cancel]
_ = (a * a⁻¹)⁻¹ * (a * ((a⁻¹ * a) * a⁻¹)) := by simp only [assoc]
_ = 1 := by rw [inv_mul_cancel, one_mul, inv_mul_cancel]
rw [← inv_mul_cancel a, ← assoc, mul_inv_cancel a, one_mul] }
