mathlib3 documentation

tactic.subtype_instance

makes the substructure axiom name from field name, by postfacing with _mem

Equations

builds instances for algebraic substructures

Example:

variables {α : Type*} [monoid α] {s : set α}

class is_submonoid (s : set α) : Prop :=
(one_mem : (1:α)  s)
(mul_mem {a b} : a  s  b  s  a * b  s)

instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
by subtype_instance
```

builds instances for algebraic substructures

Example:

variables {α : Type*} [monoid α] {s : set α}

class is_submonoid (s : set α) : Prop :=
(one_mem : (1:α)  s)
(mul_mem {a b} : a  s  b  s  a * b  s)

instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
by subtype_instance
```