RingHomLawArgs

Mathlib.Algebra.Ring.FirstIsomorphism.Basic

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 (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (S : Sort v), forall (zeroS : S), forall (oneS : S), forall (addS : forall (a : S), forall (b : S), S), forall (negS : forall (a : S), S), forall (subS : forall (a : S), forall (b : S), S), forall (mulS : forall (a : S), forall (b : S), S), forall (f : forall (x : R), S), Prop

Proof term

def RingHomLawArgs.{u,v} :
  forall (R : Sort u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (S : Sort v), forall (zeroS : S), forall (oneS : S), forall (addS : forall (a : S), forall (b : S), S), forall (negS : forall (a : S), S), forall (subS : forall (a : S), forall (b : S), S), forall (mulS : forall (a : S), forall (b : S), S), forall (f : forall (x : R), S), Prop :=
  fun R => fun zeroR => fun oneR => fun addR => fun negR => fun subR => fun mulR => fun S => fun zeroS => fun oneS => fun addS => fun negS => fun subS => fun mulS => fun f => forall (P : Prop), forall (mk : forall (hom_zero_law : @Eq.{v} S (f zeroR) zeroS), forall (hom_one_law : @Eq.{v} S (f oneR) oneS), forall (hom_add_law : forall (a : R), forall (b : R), @Eq.{v} S (f (addR a b)) (addS (f a) (f b))), forall (hom_neg_law : forall (a : R), @Eq.{v} S (f (negR a)) (negS (f a))), forall (hom_mul_law : forall (a : R), forall (b : R), @Eq.{v} S (f (mulR a b)) (mulS (f a) (f b))), P), P