pow_four_add_four_mul_pow_four — Mathlib

English

A classic factorization: a^4 + 4 b^4 = (a^2 - 2ab + 2b^2)(a^2 + 2ab + 2b^2).

Русский

Классическое разложение: a^4 + 4 b^4 = (a^2 - 2ab + 2b^2)(a^2 + 2ab + 2b^2).

LaTeX

$$$a^4 + 4b^4 = (a^2 - 2ab + 2b^2)(a^2 + 2ab + 2b^2)$$$

Lean4

/-- Sophie Germain's identity, see <https://www.cut-the-knot.org/blue/SophieGermainIdentity.shtml>.
-/
theorem pow_four_add_four_mul_pow_four : a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2) := by ring

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