Commit 2026-01-03 10:24 45f3a969

View on Github →

chore(Algebra/MonoidAlgebra/Basic): rename variables (#33516) ... and unify them within the file. As a result, lift R M A becomes lift R A M, which I think makes more sense anyway.

Estimated changes

Modified Mathlib/Algebra/FreeAlgebra.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

modified theorem AddMonoidAlgebra.algHom_ext'

modified theorem AddMonoidAlgebra.algHom_ext_iff

modified theorem AddMonoidAlgebra.coe_liftNCAlgHom

modified def AddMonoidAlgebra.lift

modified def AddMonoidAlgebra.liftMagma

modified def AddMonoidAlgebra.liftNCAlgHom

modified theorem AddMonoidAlgebra.lift_apply'

modified theorem AddMonoidAlgebra.lift_apply

modified theorem AddMonoidAlgebra.lift_def

modified theorem AddMonoidAlgebra.lift_of'

modified theorem AddMonoidAlgebra.lift_of

modified theorem AddMonoidAlgebra.lift_single

modified theorem AddMonoidAlgebra.lift_symm_apply

modified theorem AddMonoidAlgebra.lift_unique'

modified theorem AddMonoidAlgebra.lift_unique

modified theorem AddMonoidAlgebra.nonUnitalAlgHom_ext'

modified def AddMonoidAlgebra.toMultiplicativeAlgEquiv

modified def MonoidAlgebra.GroupSMul.linearMap

modified theorem MonoidAlgebra.GroupSMul.linearMap_apply

modified theorem MonoidAlgebra.algHom_ext'

modified theorem MonoidAlgebra.algHom_ext

modified theorem MonoidAlgebra.coe_algebraMap

modified theorem MonoidAlgebra.coe_liftNCAlgHom

modified def MonoidAlgebra.domCongr

modified theorem MonoidAlgebra.domCongr_apply

modified theorem MonoidAlgebra.domCongr_comp_lsingle

modified theorem MonoidAlgebra.domCongr_refl

modified theorem MonoidAlgebra.domCongr_single

modified theorem MonoidAlgebra.domCongr_support

modified theorem MonoidAlgebra.domCongr_symm

modified theorem MonoidAlgebra.domCongr_toAlgHom

modified def MonoidAlgebra.lift

modified def MonoidAlgebra.liftMagma

modified def MonoidAlgebra.liftNCAlgHom

modified theorem MonoidAlgebra.lift_apply'

modified theorem MonoidAlgebra.lift_apply

modified theorem MonoidAlgebra.lift_def

modified theorem MonoidAlgebra.lift_of

modified theorem MonoidAlgebra.lift_single

modified theorem MonoidAlgebra.lift_symm_apply

modified theorem MonoidAlgebra.lift_unique'

modified theorem MonoidAlgebra.lift_unique

modified def MonoidAlgebra.mapDomainAlgHom

modified theorem MonoidAlgebra.mapDomainAlgHom_comp

modified theorem MonoidAlgebra.mapDomainAlgHom_id

modified theorem MonoidAlgebra.mapDomain_algebraMap

modified theorem MonoidAlgebra.nonUnitalAlgHom_ext'

modified theorem MonoidAlgebra.nonUnitalAlgHom_ext

modified def MonoidAlgebra.singleOneAlgHom

modified theorem MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of

modified theorem MonoidAlgebra.single_eq_algebraMap_mul_of

modified theorem MonoidAlgebra.symm_mapRangeAlgEquiv

modified def MonoidAlgebra.toAdditiveAlgEquiv

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

Modified Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Modified Mathlib/RepresentationTheory/Basic.lean

modified theorem Representation.asAlgebraHom_def

Modified Mathlib/RepresentationTheory/Rep.lean