Minimal Axioms for a Module #
This file defines a constructor to define a Module structure on a Type with an
AddCommGroup, while proving a minimum number of equalities.
Main Definitions #
Module.ofMinimalAxioms: Define aModulestructure on a Type with an AddCommGroup by proving a minimized set of axioms
@[reducible]
def
Module.ofMinimalAxioms
{R : Type u}
{M : Type v}
[Semiring R]
[AddCommGroup M]
[SMul R M]
(smul_add : ∀ (r : R) (x y : M), r • (x + y) = r • x + r • y)
(add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x)
(mul_smul : ∀ (r s : R) (x : M), (r * s) • x = r • s • x)
(one_smul : ∀ (x : M), 1 • x = x)
:
Module R M
Define a Module structure on a Type by proving a minimized set of axioms.
Equations
- Module.ofMinimalAxioms smul_add add_smul mul_smul one_smul = Module.mk add_smul ⋯