ker_quot_to_h_mk

Mathlib.Algebra.Group.Kernel.Quotient

Packages

Module

Theorem

750

Declarations

1016

信頼境界外の sidecar

Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。

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