Commit 2023-07-24 05:38 898a8e78

View on Github →

chore: use · instead of . (#6085)

Estimated changes

modified theorem List.rel_append
modified theorem Multiset.range_add
modified theorem Multiset.range_add_eq_union
modified theorem Part.append_def
modified theorem Part.div_def
modified theorem Part.inter_def
modified theorem Part.inv_def
modified theorem Part.mod_def
modified theorem Part.mul_def
modified theorem Part.sdiff_def
modified theorem Part.union_def
modified theorem Ordinal.nfp_mul_one
modified theorem Ordinal.nfp_mul_zero