div_right — Mathlib

English

If h : SemiconjBy a x y and h' : SemiconjBy a x' y', then SemiconjBy a (x/x') (y/y').

Русский

Если h: SemiconjBy a x y и h' : SemiconjBy a x' y', то SemiconjBy a (x/x') (y/y').

LaTeX

$$Given h: SemiconjBy(a,x,y) and h': SemiconjBy(a,x',y'), then SemiconjBy(a, x/x', y/y').$$

Lean4

theorem div_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x / x') (y / y') :=
  by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact h.mul_right h'.inv_right₀

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