Back to NPA
Declaration
RingElem
Mathlib.Algebra.Ring
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
TypeProof term
inductive RingElem : Type where | unit : RingElem