mathlib4
mathlib4 copied to clipboard
chore: port Init.Propext
trafficstars
Porting anything trivial to port which contains lemmas mentioned by mathlib3's norm_num or ring.