ker_quot_to_h_mk

Mathlib.Algebra.Group.Kernel.Quotient

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 (H : Sort succ v), forall (f : forall (x : G), H), forall (a : G), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f a)) (f a)

Proof term

fun G => fun H => fun f => fun a => @Eq.refl.{succ v} H (f a)

Constants

Mathlib.Algebra.Group.Kernel.Quotient.KerQuotMk

Interface hash: sha256:cfd6d6eb23d69447f314fe61ac82546f06ebea9e29f9141aca0ae7f6c6f22e43

Mathlib.Algebra.Group.Kernel.Quotient.KerQuotToH

Interface hash: sha256:a6ba09fc274f34820e843708693ff210a4f7853713023922b527c3cc787b4b9e

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015