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: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Notation.20for.20group.28module.2Cideal.29.20quotients

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