Commit 2026-06-09 14:25 4c36dcbe

View on Github →

feat: Nat.cast commutes with addition (#39157) We prove lemmas of the form ↑m + ↑n = ↑n + ↑m in a general AddMonoidWithOne. These can be used even in otherwise noncommutative structures.

Estimated changes

added theorem Nat.addCommute_cast
added theorem Nat.cast_add_comm
added theorem Nat.cast_add_one_comm
modified theorem Ordinal.one_add_natCast