ker_quot_sound

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), forall (b : G), forall (h : @KerRel.{succ u,succ v} G H f a b), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMk.{u,v} G H f a) (@KerQuotMk.{u,v} G H f b)

Proof term

fun G => fun H => fun f => fun a => fun b => fun h => @Quotient.sound.{u} G (@KerSetoid.{u,v} G H f) a b h

Constants

Mathlib.Algebra.Group.Basic.KerRel

Interface hash: sha256:ee4d2404ac356dbae08cf67842d957a39c9c2ea01d0fac188d92ebc6da8c694a

Mathlib.Algebra.Group.Kernel.Quotient.KerQuot

Interface hash: sha256:860face55dbec0818c0d0aed68c1fe0e65dd7de77271f509ba95949348c0b9f4

Mathlib.Algebra.Group.Kernel.Quotient.KerQuotMk

Interface hash: sha256:cfd6d6eb23d69447f314fe61ac82546f06ebea9e29f9141aca0ae7f6c6f22e43

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015