map_inv₀ — Mathlib

English

If f is a homomorphism between group-with-zero structures, then f(a⁻¹) = (f a)⁻¹.

Русский

Если f гомоморфизм между группами с нулём, то f(a⁻¹) = (f(a))⁻¹.

LaTeX

$$$f a^{-1} = (f a)^{-1}$$$

Lean4

/-- A monoid homomorphism between groups with zeros sending `0` to `0` sends `a⁻¹` to `(f a)⁻¹`. -/
@[simp]
theorem map_inv₀ : f a⁻¹ = (f a)⁻¹ := by
  by_cases h : a = 0
  · simp [h, map_zero f]
  · apply eq_inv_of_mul_eq_one_left
    rw [← map_mul, inv_mul_cancel₀ h, map_one]

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