Finite Field
30 秒诊断
返回 NPA

声明

ker_quot_to_h_mk

Mathlib.Algebra.Group.Kernel.Quotient

包

2

模块

63

定理

750

声明

1016

非可信 sidecar

源文本和展示 overlay 属于展示元数据。可信证据是签名证书和 checker 结果。

陈述

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)

证明项

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

常量

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