Kim Morrison 27e1391e6d feat: complete comparison theorems for ediv/tdiv/fdiv and emod/tmod/fmod (#7199) ... This PR adds theorems comparing `Int.ediv` with `tdiv` and `fdiv`, for all signs of arguments. (Previously we just had the statements about the cases in which they agree.)		2025-02-24 01:01:40 +00:00
..
Bitwise	chore: cleanup duplicate theorems (#7113)	2025-02-18 01:46:12 +00:00
Div	feat: complete comparison theorems for ediv/tdiv/fdiv and emod/tmod/fmod (#7199)	2025-02-24 01:01:40 +00:00
Basic.lean	chore: cleanup duplicate theorems (#7113)	2025-02-18 01:46:12 +00:00
Bitwise.lean	chore: update copyrights (#5449)	2024-09-24 05:27:53 +00:00
Compare.lean	chore: upstream Std.Data.Nat (#3634)	2024-03-08 17:00:46 +00:00
Control.lean	feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)	2024-11-22 03:05:51 +00:00
Div.lean	feat: lemmas about Std.Range (#6396)	2024-12-16 03:16:46 +00:00
Dvd.lean	feat: divisibility constraint normalizer (#7092)	2025-02-15 04:20:40 +00:00
Fold.lean	feat: relate Nat.fold/foldRev/any/all to List.finRange (#6235)	2024-11-27 05:38:18 +00:00
Gcd.lean	chore: variables appearing on both sides of an iff should be implicit (#5254)	2024-09-04 08:33:24 +00:00
Lcm.lean	fix: add instances to make ac_rfl work out of the box (#3942)	2024-04-24 06:12:36 +00:00
Lemmas.lean	chore: split Int.DivModLemmas into Bootstrap and Lemmas (#7162)	2025-02-20 12:05:09 +00:00
Linear.lean	refactor: update proofs after stage0 update for #7140	2025-02-19 20:59:01 +01:00
Log2.lean	chore: don't use simp_arith when simp will do (#5256)	2024-09-04 07:56:25 +00:00
MinMax.lean	fix: add instances to make ac_rfl work out of the box (#3942)	2024-04-24 06:12:36 +00:00
Mod.lean	chore: remove unnecessary simp priorities (#6812)	2025-01-28 23:50:33 +00:00
Power2.lean	chore: cleanup duplicate theorems (#7113)	2025-02-18 01:46:12 +00:00
Simproc.lean	fix: replace unary Nat.succ simp rules with simprocs (#3808)	2024-04-04 23:15:26 +00:00
SOM.lean