Markus Himmel 674c7ef1d0 feat: Int.gcd/Int.lcm lemmas (#7802) ... This PR adds `Int.gcd` and `Int.lcm` variants of all `Nat.gcd` and `Nat.lcm` lemmas.		2025-04-04 12:44:59 +00:00
..
Bitwise	doc: review Int docstrings (#7568)	2025-03-20 14:04:56 +00:00
DivMod	feat: Int.gcd/Int.lcm lemmas (#7802)	2025-04-04 12:44:59 +00:00
Basic.lean	doc: docstring review for IntCast, NatCast, and for loops (#7645)	2025-03-25 07:58:37 +00:00
Bitwise.lean	feat: revision of Nat/Int lemmas (#7435)	2025-03-12 05:52:09 +00:00
Compare.lean	feat: Ord-related instances for various types (#7687)	2025-03-28 13:31:09 +00:00
Cooper.lean	feat: Int.gcd/Int.lcm lemmas (#7802)	2025-04-04 12:44:59 +00:00
DivMod.lean	chore: split Int.DivModLemmas into Bootstrap and Lemmas (#7162)	2025-02-20 12:05:09 +00:00
Gcd.lean	feat: Int.gcd/Int.lcm lemmas (#7802)	2025-04-04 12:44:59 +00:00
Lemmas.lean	chore: remove @[simp] from Int.neg_mul and Int.mul_neg (#7559)	2025-03-19 09:21:18 +00:00
LemmasAux.lean	feat: add BitVec.umulOverflow and BitVec.smulOverflow definitions and additional theorems (#7659)	2025-04-03 08:42:52 +00:00
Linear.lean	feat: Int.gcd/Int.lcm lemmas (#7802)	2025-04-04 12:44:59 +00:00
OfNat.lean	fix: assert that nonlinear Nat terms are nonneg in cutsat (#7561)	2025-03-19 00:52:04 +00:00
Order.lean	feat: Int.gcd/Int.lcm lemmas (#7802)	2025-04-04 12:44:59 +00:00
Pow.lean	feat: Int.gcd/Int.lcm lemmas (#7802)	2025-04-04 12:44:59 +00:00