Finite Field
30 秒诊断
返回 NPA

模块

Mathlib.Algebra.Group.Kernel.Quotient.Hom

npa-mathlib

包

2

模块

63

定理

750

声明

1016

非可信 sidecar

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

定理

1

定义

0

归纳类型

0

公理

1

声明

ker_quot_to_h_mul

forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), for...

theorem

Eq.rec

axiom

哈希

source
sha256:83535d4f2ef8ed1a9b97f6145b87923c449d502480695320f9046929dba51be2
certificateFile
sha256:cd20fd6f13cb1fbb6d5269bafea245cd6441ced5fc3b91c1a5bb5aa961fe9c06
export
sha256:2a0178a6cd6a9fff1e449bffb7a62e25d4e4a944ceb514083db0bcf5b0229700
axiomReport
sha256:b8556fe24d881da2124391b4b0d69d4d22f988483234a12d4f565c15909305e6
certificate
sha256:ed2a9ba856a0437961f5b62b26d755e26f5a526274d3b7f0cb2f6f5d960453f7

源文本

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Kernel.Quotient
import Mathlib.Algebra.Group.Kernel.Quotient.Mul
import Mathlib.Algebra.Group.Kernel.Quotient.Group

theorem ker_quot_to_h_mul.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q1 q2)) (mulH (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2)) :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun hom_args => @Quotient.indProp.{u} G (@KerSetoid.{u,v} G H f) (fun (q1 : @KerQuot.{u,v} G H f) => forall (q2 : @KerQuot.{u,v} G H f), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q1 q2)) (mulH (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2))) (fun (a : G) => @Quotient.indProp.{u} G (@KerSetoid.{u,v} G H f) (fun (q2 : @KerQuot.{u,v} G H f) => @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@KerQuotMk.{u,v} G H f a) q2)) (mulH (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f a)) (@KerQuotToH.{u,v} G H f q2))) (fun (b : G) => @hom_mul.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args a b))