SecondIsoTheoremEvidence

Mathlib.Algebra.Group.SecondIsomorphism

Packages

Module

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 succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (Hpred : forall (x : G), Prop), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), Prop

Proof term

fun G => fun one => fun mul => fun inv => fun Hpred => fun N => fun group_args => fun h_args => fun normal_args => forall (P : Prop), forall (mk : forall (kernel_evidence : @SecondIsoKernelEvidence.{u} G one mul inv N group_args normal_args Hpred), forall (image_evidence : @SecondIsoImageEvidence.{u} G one mul inv N group_args normal_args Hpred), P), P