test_subgroup_import_check
Provedtest
Test if Subgroup is available
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem test_subgroup_import_check {G : Type _} [Group G] (H : Subgroup G) : H.carrier.Nonempty := by sorryTest if Subgroup is available
import Mathlib.Analysis.Complex.Basic
theorem test_subgroup_import_check {G : Type _} [Group G] (H : Subgroup G) : H.carrier.Nonempty := by sorry