div — Mathlib

English

If a and b are squares in a DivisionComMonoid, then a/b is a square.

Русский

Если a и b — квадраты в DivisionCommMonoid, то a/b — квадрат.

LaTeX

$$$\operatorname{IsSquare}(a) \rightarrow \operatorname{IsSquare}(b) \rightarrow \operatorname{IsSquare}(a/b)$$$

Lean4

@[to_additive (attr := aesop unsafe 90%)]
theorem div [DivisionCommMonoid α] {a b : α} (ha : IsSquare a) (hb : IsSquare b) : IsSquare (a / b) := by
  aesop (add simp div_eq_mul_inv)

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