smul_inv₀ — Mathlib

English

If c ∈ G₀ and x ∈ G₀', then (c • x)⁻¹ = c⁻¹ • x⁻¹, with the obvious zero cases handled by inv 0 = 0.

Русский

Для c ∈ G₀ и x ∈ G₀' верно (c • x)⁻¹ = c⁻¹ • x⁻¹, за исключением случаев, когда один из факторов равен нулю (inv 0 = 0).

LaTeX

$$$\\smulInvZero : (c:\\, G_0)\\ (x:\\, G_0')\\; (c \\cdot x)^{-1} = c^{-1} \\cdot x^{-1}$$$

Lean4

theorem smul_inv₀ (c : G₀) (x : G₀') : (c • x)⁻¹ = c⁻¹ • x⁻¹ :=
  by
  obtain rfl | hc := eq_or_ne c 0
  · simp only [inv_zero, zero_smul]
  obtain rfl | hx := eq_or_ne x 0
  · simp only [inv_zero, smul_zero]
  · refine inv_eq_of_mul_eq_one_left ?_
    rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]

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