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 a Module structure on a Type with an AddCommGroup by proving a minimized set of axioms

@[reducible, inline]

abbrev 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

• One or more equations did not get rendered due to their size.