ring_crt_intersection_intro

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

Proof term

theorem ring_crt_intersection_intro.{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 (left_kernel : @Eq.{v} RI (modI x) zeroI), forall (right_kernel : @Eq.{w} RJ (modJ x) zeroJ), @RingCrtIntersectionPred.{u,v,w} R RI RJ zeroI zeroJ modI modJ x :=
  fun R => fun RI => fun RJ => fun zeroI => fun zeroJ => fun modI => fun modJ => fun x => fun left_kernel => fun right_kernel => fun (Q : Prop) => fun (mk : forall (left_kernel_arg : @Eq.{v} RI (modI x) zeroI), forall (right_kernel_arg : @Eq.{w} RJ (modJ x) zeroJ), Q) => mk left_kernel right_kernel

Constants

Mathlib.Algebra.Ring.ChineseRemainder.RingCrtIntersectionPred

Interface hash: sha256:d7078db886688e39bc3bd8cd7fe1681a308fc3ed146e2d568a37431fd39df6f1

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015