Def Module.ofCore

Modification history

2023-12-07 14:58

Mathlib/Algebra/Module/Basic.lean

refactor(Algebra/Module): Move `Module.ofCore` to a MinimalAxioms file, and rename it `ofMinimalAxioms` (#8853) …

Deleted Module.ofCore View on Github →

2022-12-31 22:33

Mathlib/Algebra/Module/Basic.lean

feat: port Algebra.Module.Basic (#1169) …

Added Module.ofCore View on Github →