isUnit_smul_iff — Mathlib

English

Let g ∈ α (a group) and m ∈ β (a monoid with α-action). Then IsUnit(g • m) holds if and only if IsUnit(m).

Русский

Пусть g ∈ α (группа) и m ∈ β (моноид с действием α). Тогда IsUnit(g • m) эквивалентно IsUnit(m).

LaTeX

$$$ \forall g \in \alpha,\forall m \in \beta,\ IsUnit(g \cdot m) \iff IsUnit(m). $$$

Lean4

@[simp]
theorem isUnit_smul_iff (g : α) (m : β) : IsUnit (g • m) ↔ IsUnit m :=
  ⟨fun h => inv_smul_smul g m ▸ h.smul g⁻¹, IsUnit.smul g⟩

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