Theorems · Definition · group theory

ofAddUnits_addUnits_gci

{M : Type u_1} → [inst : AddMonoid M] → GaloisCoinsertion AddSubgroup.ofAddUnits AddSubmonoid.addUnits

A Galois coinsertion exists between the coercion from an additive subgroup of additive units to an additive submonoid and the reduction from an additive submonoid to its unit group.

Defined in

Mathlib.Algebra.Group.Submonoid.Units

Cited by

9 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound

Assumes

AddMonoid