Commit 2023-12-07 14:58 49c57216

View on Github →

refactor(Algebra/Module): Move Module.ofCore to a MinimalAxioms file, and rename it ofMinimalAxioms (#8853) This makes it consistent with Ring, Field and Group.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Basic.lean

deleted structure Module.Core

deleted def Module.ofCore

Created Mathlib/Algebra/Module/MinimalAxioms.lean

added def Module.ofMinimalAxioms

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean