Finite Field
30 秒诊断
返回 NPA

模块

Mathlib.Algebra.Group.Quotient

npa-mathlib

包

2

模块

63

定理

750

声明

1016

非可信 sidecar

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

定理

1

定义

3

归纳类型

0

公理

1

声明

NormalSetoid

forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop...

definition

NormalQuot

forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop...

definition

NormalQuotMk

forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop...

definition

normal_quot_sound

forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop...

theorem

Eq.rec

axiom

哈希

source
sha256:d05276fa74eb6d236c25c109f09c31bfa5ba7239893af26921b6134bdc7e0061
certificateFile
sha256:95564c1e3a7172a768384daa7392e06895df59581cba4e532ddd9f1c722f4f31
export
sha256:14d52188e958a89a9f87ad32a12c2738a73c0e185d68bcd390875bf4dea7f4de
axiomReport
sha256:9fdeea3b7c832309cc77d8a52df14c8bdf8c3cc2ade0673e86e2d27b1d6f089e
certificate
sha256:6fc7c518e7eaa04e792bb1d4dd3af7b4f5c4987136a118ce98a75d601c4feb19

源文本

import Std.Logic.Eq
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Subgroup

def NormalSetoid.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), @Setoid.{u} G :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => @Setoid.mk.{u} G (@NormalRel.{succ u} G one mul inv N) (fun (P : Prop) => fun (mk_equiv : forall (refl_arg : forall (x : G), @NormalRel.{succ u} G one mul inv N x x), forall (symm_arg : forall (x : G), forall (y : G), forall (p : @NormalRel.{succ u} G one mul inv N x y), @NormalRel.{succ u} G one mul inv N y x), forall (trans_arg : forall (x : G), forall (y : G), forall (z : G), forall (p : @NormalRel.{succ u} G one mul inv N x y), forall (q : @NormalRel.{succ u} G one mul inv N y z), @NormalRel.{succ u} G one mul inv N x z), P) => mk_equiv (@normal_rel_refl.{succ u} G one mul inv group_args N normal_args) (@normal_rel_symm.{succ u} G one mul inv group_args N normal_args) (@normal_rel_trans.{succ u} G one mul inv group_args N normal_args))

def NormalQuot.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), Sort succ u :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => @Quotient.{u} G (@NormalSetoid.{u} G one mul inv N group_args normal_args)

def NormalQuotMk.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (a : G), @NormalQuot.{u} G one mul inv N group_args normal_args :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun a => @Quotient.mk.{u} G (@NormalSetoid.{u} G one mul inv N group_args normal_args) a

theorem normal_quot_sound.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (a : G), forall (b : G), forall (h : @NormalRel.{succ u} G one mul inv N a b), @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args a) (@NormalQuotMk.{u} G one mul inv N group_args normal_args b) :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun a => fun b => fun h => @Quotient.sound.{u} G (@NormalSetoid.{u} G one mul inv N group_args normal_args) a b h