Theorems · Definition · group theory

AddSubgroup.copy

{G : Type u_1} → [inst : AddGroup G] → (K : AddSubgroup G) → (s : Set G) → s = ↑K → AddSubgroup G

Copy of an additive subgroup with a new carrier equal to the old one. Useful to fix definitional equalities

Defined in

Mathlib.Algebra.Group.Subgroup.Defs

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

AddGroup