Back to NPA
Declaration
ring_crt_intersection_to_kernel
Mathlib.Algebra.Ring.ChineseRemainder
Packages
2
Module
63
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 succ u), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (zeroI : RI), forall (zeroJ : RJ), forall (zeroP : P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (x : R), forall (left_kernel : @Eq.{succ v} RI (modI x) zeroI), forall (right_kernel : @Eq.{succ w} RJ (modJ x) zeroJ), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroPProof term
theorem ring_crt_intersection_to_kernel.{p,u,v,w} :
forall (R : Sort succ u), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (zeroI : RI), forall (zeroJ : RJ), forall (zeroP : P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (x : R), forall (left_kernel : @Eq.{succ v} RI (modI x) zeroI), forall (right_kernel : @Eq.{succ w} RJ (modJ x) zeroJ), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP :=
fun R => fun RI => fun RJ => fun P => fun zeroI => fun zeroJ => fun zeroP => fun pair => fun modI => fun modJ => fun zero_pair => fun x => fun left_kernel => fun right_kernel => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) (pair zeroI zeroJ) zeroP (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI x) zeroI (modJ x) zeroJ left_kernel right_kernel) zero_pair