Finite Field
30 秒诊断
返回 NPA

声明

ring_first_iso_phi_injective

Mathlib.Algebra.Ring.FirstIsomorphism

包

2

模块

63

定理

750

声明

1016

非可信 sidecar

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

陈述

forall (R : Sort succ u), forall (S : Sort succ v), forall (f : forall (x : R), S), forall (q1 : @RingKerQuot.{u,v} R S f), forall (q2 : @RingKerQuot.{u,v} R S f), forall (h : @Eq.{succ v} S (@RingKerQuotToS.{u,v} R S f q1) (@RingKerQuotToS.{u,v} R S f q2)), @Eq.{succ u} (@RingKerQuot.{u,v} R S f) q1 q2

证明项

theorem ring_first_iso_phi_injective.{u,v} :
  forall (R : Sort succ u), forall (S : Sort succ v), forall (f : forall (x : R), S), forall (q1 : @RingKerQuot.{u,v} R S f), forall (q2 : @RingKerQuot.{u,v} R S f), forall (h : @Eq.{succ v} S (@RingKerQuotToS.{u,v} R S f q1) (@RingKerQuotToS.{u,v} R S f q2)), @Eq.{succ u} (@RingKerQuot.{u,v} R S f) q1 q2 :=
  fun R => fun S => fun f => @first_iso_phi_injective.{u,v} R S f

常量

Mathlib.Algebra.Ring.FirstIsomorphism.Basic.RingKerQuot

Interface hash: sha256:aca2a22cfa356002de43459a02a4d82f3d11d7a363cd03723dcc16c4c933dbac

Mathlib.Algebra.Ring.FirstIsomorphism.Basic.RingKerQuotToS

Interface hash: sha256:7c31b5ce56066fb117a86bc8f8ccaf2979ea2afd628668a518635b7ce8fa61ad

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015