ring_crt_intersection_left

Mathlib.Algebra.Ring.ChineseRemainder

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 (R : Sort u), forall (RI : Sort v), forall (RJ : Sort w), forall (zeroI : RI), forall (zeroJ : RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (x : R), forall (h : @RingCrtIntersectionPred.{u,v,w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{v} RI (modI x) zeroI

Proof term

theorem ring_crt_intersection_left.{u,v,w} :
  forall (R : Sort u), forall (RI : Sort v), forall (RJ : Sort w), forall (zeroI : RI), forall (zeroJ : RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (x : R), forall (h : @RingCrtIntersectionPred.{u,v,w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{v} RI (modI x) zeroI :=
  fun R => fun RI => fun RJ => fun zeroI => fun zeroJ => fun modI => fun modJ => fun x => fun h => h (@Eq.{v} RI (modI x) zeroI) (fun (left_kernel_arg : @Eq.{v} RI (modI x) zeroI) => fun (right_kernel_arg : @Eq.{w} RJ (modJ x) zeroJ) => left_kernel_arg)

Constants

Mathlib.Algebra.Ring.ChineseRemainder.RingCrtIntersectionPred

Interface hash: sha256:d7078db886688e39bc3bd8cd7fe1681a308fc3ed146e2d568a37431fd39df6f1

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015