Finite Field
30-sec diagnosis
Back to NPA

Declaration

subgroup_equiv_refl

Mathlib.Algebra.Group.Subgroup.Order

Packages

2

Module

63

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Statement

forall (G : Sort u), forall (H : forall (x : G), Prop), @SubgroupEquiv.{u} G H H

Proof term

fun G => fun H => @subgroup_equiv_intro.{u} G H H (@subgroup_le_refl.{u} G H) (@subgroup_le_refl.{u} G H)

Constants

Mathlib.Algebra.Group.Subgroup.Order.SubgroupEquiv

Interface hash: sha256:f2a86a1beb908a58606023f72dfcaa93bfda96dd3ef597fdb8c2962dabfabfe9