mul — Mathlib

English

If a and b are squares in a commutative semigroup, then a·b is a square.

Русский

Если элементы a и b — квадраты, то их произведение a·b — квадрат.

LaTeX

$$\[IsSquare a \rightarrow IsSquare b \rightarrow IsSquare (a b)\]$$

Lean4

@[to_additive (attr := aesop unsafe 90%)]
theorem mul [CommSemigroup α] {a b : α} : IsSquare a → IsSquare b → IsSquare (a * b) := fun ⟨r, _⟩ ⟨s, _⟩ =>
  ⟨r * s, by simp_all [mul_mul_mul_comm]⟩

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