pow_four_add_four_mul_pow_four' — Mathlib

English

A variant form of Sophie Germain’s identity expressed with alternative signs for a and b.

Русский

Вариант формы идентичности Софи Геpманa с альтернативными знаками для a и b.

LaTeX

$$The prime form: $a^4+4b^4$ equals the product of two quadratics with alternate signs, as given in the theorem.$$

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 ^ 2 - 2 * a * b + 2 * b ^ 2) * (a ^ 2 + 2 * a * b + 2 * b ^ 2) := by ring

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