Merge pull request #2206 from Alizter/ps/rr/being_trivial_is_invarian…

…t_under_iso being trivial is invariant under iso
HoTT · Jan 29, 2025 · 77c8a6d · 77c8a6d
2 parents 03ff069 + 5db7e15
commit 77c8a6d
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
@@ -612,6 +612,16 @@ Proof.
   1,2: apply istrivial_iff_grp_iso_trivial; exact _.
 Defined.
 
+Definition istrivial_grp_iso {G H : Group} (J : Subgroup G) (K : Subgroup H)
+  (e : subgroup_group J $<~> subgroup_group K)
+  : IsTrivialGroup J -> IsTrivialGroup K.
+Proof.
+  intros triv.
+  apply istrivial_iff_grp_iso_trivial in triv.
+  apply istrivial_iff_grp_iso_trivial.
+  exact (triv $oE e^-1$).
+Defined.
+
 (** ** Maximal Subgroups *)
 
 (** Every group is a (maximal) subgroup of itself. *)