# 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

source
@[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.

Instances For