Mathlib v3 is deprecated. Go to Mathlib v4

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 def matrix.to_lie_algebra
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
modified theorem quotient_group.eq'
modified theorem quotient_group.forall_coe
modified theorem quotient_group.induction_on
modified def quotient_group.mk
modified theorem quotient_group.out_eq'
modified theorem subgroup.index_eq_card
modified theorem is_p_group.index
modified theorem quotient_group.coe_mk'
modified theorem quotient_group.eq_one_iff
modified def quotient_group.mk'
modified def adic_completion.eval
modified def adic_completion
modified theorem submodule.le_comap_mkq
modified def submodule.liftq
modified theorem submodule.linear_map_qext
modified theorem submodule.map_liftq
modified def submodule.mapq_linear
modified def submodule.mkq
modified theorem submodule.quot_hom_ext
modified def submodule.quotient.mk
modified theorem submodule.quotient.mk_add
modified theorem submodule.quotient.mk_neg
modified theorem submodule.quotient.mk_smul
modified theorem submodule.quotient.mk_sub
modified theorem submodule.quotient.mk_zero
deleted def submodule.quotient
modified def class_group
modified theorem ideal.ker_lift.map_smul
modified def ideal.ker_lift_alg
modified def ideal.quotient.mkₐ
modified theorem ideal.quotient.mkₐ_ker
modified def ring_hom.ker_lift
modified def ideal.quotient.factor
modified def ideal.quotient.mk
modified theorem ideal.quotient.mk_eq_mk
modified theorem ideal.quotient.ring_hom_ext
deleted def ideal.quotient
modified theorem valuation.comap_on_quot_eq