Commit 2023-11-29 06:54 79254c97

View on Github →

fix: lean4-ify names of inductive constructors (#8652) These inductive types carry data, so these should be functionCase not theorem_case. It seems that mathport didn't do this.

Estimated changes

Modified Mathlib/Algebra/FreeAlgebra.lean

modified def FreeAlgebra.Pre.hasCoeSemiring

modified def FreeAlgebra.Pre.hasOne

modified def FreeAlgebra.Pre.hasSmul

modified def FreeAlgebra.Pre.hasZero

Modified Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

modified theorem CategoryTheory.FreeMonoidalCategory.unit_eq_unit

Modified Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/Geometry/Euclidean/MongePoint.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean