Def IsSubgroup.trivial

Modification history

2023-08-10 19:52

Mathlib/Deprecated/Subgroup.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified IsSubgroup.trivial View on Github →

2023-01-27 13:20

Mathlib/Deprecated/Subgroup.lean

feat: port `Deprecated.Subgroup` (#1876)

Added IsSubgroup.trivial View on Github →