Theorems · Theorem · group theory
FreeGroup.range_lift_eq_closure
∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β}, (FreeGroup.lift f).range = Subgroup.closure (Set.range f)- Defined in
- Mathlib.GroupTheory.FreeGroup.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Equivstatement · cited by 8,337
- Groupstatement and proof · cited by 6,238
- Set.rangestatement and proof · cited by 4,705
- MonoidHomstatement · cited by 3,629
- Subgroupstatement · cited by 3,593
- le_antisymmproof · cited by 2,068
- MonoidHom.rangestatement and proof · cited by 314
- Subgroup.closurestatement · cited by 196
- FreeGroupstatement · cited by 132
- Subgroup.subset_closureproof · cited by 53
- FreeGroup.ofproof · cited by 39
Cited by5
Results whose statement or proof uses this declaration.
- FreeGroup.closure_range_ofproof · cited by 2
- FreeGroup.lift_surjective_of_surjectiveproof · cited by 1
- FreeGroup.closure_eq_rangeproof · cited by 1
- FreeGroup.range_mapproof · cited by 1
- FreeGroup.lift_surjective_iff_closure_range_eq_topproof · cited by 1