inv — Mathlib

English

A multiplicative congruence preserves inversion: if x is related to y, then x^{-1} is related to y^{-1}.

Русский

Умножающая конгруэнция сохраняет инверсию: если x связано с y, то x^{-1} связано с y^{-1}.

LaTeX

$$$c\\,x\\,y \\Rightarrow c\\,x^{-1}\\,y^{-1}$$$

Lean4

/-- Multiplicative congruence relations preserve inversion. -/
@[to_additive /-- Additive congruence relations preserve negation. -/
    ]
protected theorem inv {x y} (h : c x y) : c x⁻¹ y⁻¹ :=
  c.map_of_mul_left_rel_one Inv.inv (fun x => by simp only [inv_mul_cancel, c.refl 1]) h

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