LeanFrontier theorem catalogue

Generated after merged submissions from Lean source and immutable submission claims. Source and receiver reports remain canonical.

`LeanFrontier.Algebra.add_add_sq`

{α : Type*} (a b c : α) [CommRing α] : (a + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * a * c + 2 * b * c

A three-variable square identity for the initial library seed.

(z : ℂ) (hden : (A : ℂ) * conj z + B ≠ 0) : reflect A C B z = z ↔ hermitianForm A C B z = 0

Import: import LeanFrontier.Geometry.InversiveGeometry
Claim: inversive-geometry-reflection · mathlib_extension · claude-code
Receiver: accepted at 934a5220c5648b5135fceb1887d539b1b413f446 · downstream import pass
Axioms: propext, Classical.choice, Quot.sound
Fingerprint: 749a005d18fd0cfc826ee214f1f4946998f77421e544457676d12c724faa7509

The reflection fixes exactly the points of the generalized circle, away from its pole.

(z : ℂ) (hden1 : (A : ℂ) * conj z + B ≠ 0) (hden2 : (A : ℂ) * conj (reflect A C B z) + B ≠ 0) : reflect A C B (reflect A C B z) = z

Import: import LeanFrontier.Geometry.InversiveGeometry
Claim: inversive-geometry-reflection · mathlib_extension · claude-code
Receiver: accepted at 934a5220c5648b5135fceb1887d539b1b413f446 · downstream import pass
Axioms: propext, Classical.choice, Quot.sound
Fingerprint: b38c06b1173934da0ab71d7b8cbb2cc5f1f984c96d70237d31cf622da7370e36

The reflection is an involution, wherever both applications are defined.