Commit 2023-09-16 19:24 2f19a6b1

View on Github →

feat(AddMonoidAlgebra*): add notation R[A] for addMonoidAlgebra R A (#7203) Introduce the notation R[A] for AddMonoidAlgebra R A. This is to align Mathlibs notation with the standard notation for group ring. The notation is scoped in AddMonoidAlgebra and there is no analogous notation for MonoidAlgebra. I only used the notation for single-character R and As and only in the range [a-zA-Z]. The extra lines are all in Mathlib/Algebra/MonoidAlgebra/Basic.lean. They are accounted for by extra text in the doc-module and the actual notation. Affected files:

Counterexamples/ZeroDivisorsInAddMonoidAlgebras
Algebra/AlgebraicCard
Algebra/MonoidAlgebra/Basic
Algebra/MonoidAlgebra/Degree
Algebra/MonoidAlgebra/Division
Algebra/MonoidAlgebra/Grading
Algebra/MonoidAlgebra/NoZeroDivisors
Algebra/MonoidAlgebra/Support
Data/Polynomial/AlgebraMap
Data/Polynomial/Basic
Data/Polynomial/Eval
Data/Polynomial/Laurent
RingTheory/FiniteType

Estimated changes

Modified Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

Modified Mathlib/Algebra/AlgebraicCard.lean

modified theorem Algebraic.cardinal_mk_le_mul

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

modified theorem AddMonoidAlgebra.algHom_ext'

modified theorem AddMonoidAlgebra.algHom_ext

modified theorem AddMonoidAlgebra.algHom_ext_iff

modified def AddMonoidAlgebra.domCongr

modified theorem AddMonoidAlgebra.induction_on

modified def AddMonoidAlgebra.lift

modified def AddMonoidAlgebra.liftNC

modified theorem AddMonoidAlgebra.lift_symm_apply

modified theorem AddMonoidAlgebra.lift_unique'

modified theorem AddMonoidAlgebra.lift_unique

modified theorem AddMonoidAlgebra.mul_apply

modified theorem AddMonoidAlgebra.mul_apply_antidiagonal

modified theorem AddMonoidAlgebra.mul_def

modified theorem AddMonoidAlgebra.mul_single_apply

modified theorem AddMonoidAlgebra.mul_single_apply_aux

modified theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add

modified theorem AddMonoidAlgebra.mul_single_zero_apply

modified theorem AddMonoidAlgebra.nat_cast_def

modified theorem AddMonoidAlgebra.nonUnitalAlgHom_ext'

modified theorem AddMonoidAlgebra.nonUnitalAlgHom_ext

modified def AddMonoidAlgebra.of'

modified def AddMonoidAlgebra.of

modified def AddMonoidAlgebra.ofMagma

modified theorem AddMonoidAlgebra.one_def

modified theorem AddMonoidAlgebra.ringHom_ext'

modified theorem AddMonoidAlgebra.ringHom_ext

modified def AddMonoidAlgebra.singleHom

modified def AddMonoidAlgebra.singleZeroRingHom

modified theorem AddMonoidAlgebra.single_mul_apply

modified theorem AddMonoidAlgebra.single_mul_apply_aux

modified theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add

modified theorem AddMonoidAlgebra.single_zero

modified theorem AddMonoidAlgebra.single_zero_mul_apply

modified theorem AddMonoidAlgebra.sum_single

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

modified def AddMonoidAlgebra.infDegree

modified theorem AddMonoidAlgebra.le_infDegree_add

modified theorem AddMonoidAlgebra.le_infDegree_mul

modified def AddMonoidAlgebra.supDegree

modified theorem AddMonoidAlgebra.supDegree_add_le

modified theorem AddMonoidAlgebra.supDegree_mul_le

Modified Mathlib/Algebra/MonoidAlgebra/Division.lean

modified theorem AddMonoidAlgebra.add_divOf

modified theorem AddMonoidAlgebra.divOf_add

modified theorem AddMonoidAlgebra.divOf_add_modOf

modified theorem AddMonoidAlgebra.divOf_apply

modified theorem AddMonoidAlgebra.divOf_zero

modified theorem AddMonoidAlgebra.modOf_add_divOf

modified theorem AddMonoidAlgebra.modOf_apply_add_self

modified theorem AddMonoidAlgebra.modOf_apply_of_exists_add

modified theorem AddMonoidAlgebra.modOf_apply_of_not_exists_add

modified theorem AddMonoidAlgebra.modOf_apply_self_add

modified theorem AddMonoidAlgebra.mul_of'_divOf

modified theorem AddMonoidAlgebra.mul_of'_modOf

modified theorem AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero

modified theorem AddMonoidAlgebra.of'_mul_divOf

modified theorem AddMonoidAlgebra.of'_mul_modOf

modified theorem AddMonoidAlgebra.support_divOf

modified theorem AddMonoidAlgebra.zero_divOf

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

modified def AddMonoidAlgebra.decomposeAux

modified theorem AddMonoidAlgebra.mem_gradeBy_iff

modified theorem AddMonoidAlgebra.mem_grade_iff'

modified theorem AddMonoidAlgebra.mem_grade_iff

Modified Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

modified theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

modified theorem AddMonoidAlgebra.mem_span_support'

modified theorem AddMonoidAlgebra.mem_span_support

modified theorem AddMonoidAlgebra.support_mul

modified theorem AddMonoidAlgebra.support_mul_single

modified theorem AddMonoidAlgebra.support_single_mul

Modified Mathlib/Data/Polynomial/AlgebraMap.lean

modified def Polynomial.toFinsuppIsoAlg

Modified Mathlib/Data/Polynomial/Basic.lean

modified theorem Polynomial.ofFinsupp_erase

modified theorem Polynomial.ofFinsupp_sum

modified def Polynomial.toFinsuppIso

Modified Mathlib/Data/Polynomial/Eval.lean

modified theorem Polynomial.eval₂_ofFinsupp

Modified Mathlib/Data/Polynomial/Laurent.lean

Modified Mathlib/RingTheory/FiniteType.lean

modified theorem AddMonoidAlgebra.exists_finset_adjoin_eq_top

modified theorem AddMonoidAlgebra.fg_of_finiteType

modified theorem AddMonoidAlgebra.mem_adjoin_support

modified theorem AddMonoidAlgebra.support_gen_of_gen'

modified theorem AddMonoidAlgebra.support_gen_of_gen