Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
∃ u. ∃ v. a + m · u = b + m · vOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists u v. a + m * u = b + m * vThe 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
none
Checked theorems using this definition
CG0001 · mod_eq_cancel_gcd_cofactorCG0002 · linear_congruence_solution_class_iff_reduced_modulusCG0003 · linear_congruence_reduced_representative_existsCG0005 · linear_congruence_bounded_residue_parametrizedCG0007 · linear_congruence_bounded_solutions_parametrizedCG0008 · linear_congruence_exact_bounded_enumeration_existsCG0009 · linear_congruence_zero_modulus_nonzero_coefficient_uniqueCG000A · linear_congruence_zero_modulus_zero_coefficient_iffCG000B · linear_congruence_modulus_one_bounded_iff_zeroCG000C · fermat_little_all_inputs