Commit 2021-12-04 01:52 23dfe700

View on Github →

feat(*): A ⧸ B notation for quotients in algebra (#10501) We introduce a class has_quotient that provides (U+29F8 BIG SOLIDUS) notation for quotients, e.g. if H : subgroup G then quotient_group.quotient H is now written as G ⧸ H. Thanks to @jcommelin for suggesting the initial design. Zulip thread:

Estimated changes

modified theorem norm_mk_lt
modified theorem norm_mk_zero
modified theorem quotient_norm_add_le
modified theorem quotient_norm_neg
modified theorem quotient_norm_nonneg
modified theorem quotient_norm_sub_rev