Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
u · V + 1 = U · v ∧ (a · v = b · u + E ∧ b · U = a · V + F) ∨ U · v + 1 = u · V ∧ (b · u = a · v + E ∧ a · V = b · U + F)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(((u * V + 1 = U * v) /\ ((a * v = b * u + E) /\ (b * U = a * V + F)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + E) /\ (a * V = b * U + F))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
Checked theorems using this definition
BA0005 · cf_approximation_empty_matrix_identityBA0006 · cf_approximation_prepend_identityBA0008 · cf_approximation_identity_entry_transportBA0009 · cf_approximation_identity_current_absolute_errorBA000B · cf_approximation_first_recurrence_error_invariantBA0025 · cf_approximation_alternating_identity_best_approximation