ring_first_iso_phi_hits_image

Mathlib.Algebra.Ring.FirstIsomorphism

Packages

Module

Theorem

750

Declarations

1016

信頼境界外の sidecar

Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。

Statement

forall (R : Sort succ u), forall (S : Sort succ v), forall (f : forall (x : R), S), forall (q : @RingKerQuot.{u,v} R S f), @RingImagePred.{succ u,succ v} R S f (@RingKerQuotToS.{u,v} R S f q)

Proof term

theorem ring_first_iso_phi_hits_image.{u,v} :
  forall (R : Sort succ u), forall (S : Sort succ v), forall (f : forall (x : R), S), forall (q : @RingKerQuot.{u,v} R S f), @RingImagePred.{succ u,succ v} R S f (@RingKerQuotToS.{u,v} R S f q) :=
  fun R => fun S => fun f => @first_iso_phi_hits_image.{u,v} R S f

Constants

Mathlib.Algebra.Ring.FirstIsomorphism.Basic.RingImagePred

Interface hash: sha256:efd5770d70b83a8d9d15ac039cb28a52ddc9b1fccd28df0448d4c90bb9fec646

Mathlib.Algebra.Ring.FirstIsomorphism.Basic.RingKerQuot

Interface hash: sha256:aca2a22cfa356002de43459a02a4d82f3d11d7a363cd03723dcc16c4c933dbac

Mathlib.Algebra.Ring.FirstIsomorphism.Basic.RingKerQuotToS

Interface hash: sha256:7c31b5ce56066fb117a86bc8f8ccaf2979ea2afd628668a518635b7ce8fa61ad