Theorems · Definition · group theory

Subgroup.copy

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

Copy of a 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

Group