Commit 2026-04-10 07:34 bc6b91e7

View on Github →

feat(RingTheory/FormalGroup): definition and examples of formal group (#35912)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/FormalGroup/Basic.lean

added def FormalGroup.Point

added def FormalGroup.map

added def FormalGroup.𝔾ₐ

added def FormalGroup.𝔾ₘ

added structure FormalGroup

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

added theorem MvPowerSeries.HasSubst.X_X

added theorem MvPowerSeries.HasSubst.cons_subst_zero_left

added theorem MvPowerSeries.HasSubst.cons_subst_zero_right

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Ring/NamePowerVars.lean

added def Mathlib.Tactic.elabNamePowerSeriesVariablesOver

Modified docs/references.bib