(G : AbGroup) : Subgroup G -> AbGroup := fun H => Build_AbGroup H _. #[warnings="-uniform-inheritance"] Coercion : Subgroup >-> AbGroup. Global Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G) : IsNormalSubgroup H. Proof. intros x y h. by rewrite ab_comm. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.