Properties of `OrderedCommRings`#1303

Open

LorenzoMolena wants to merge 24 commits into

agda:masterfrom

LorenzoMolena:ocr-update

Commits on Apr 2, 2026

add properties of OCR and OCR-morphisms, including univalence and canonical embedding from the integers
LorenzoMolena
committed

Commits on Apr 4, 2026

add `isUniqueFromℤOCR` and `isUniqueFromℤOCRMono` in `CanonicalMonoFromℤ`
LorenzoMolena
committed
call the ring solver only when there is not already a specific lemma solving the equality ; use `_<+[_]`, `_≤·[_,_]`, etc. in equational reasoning ; shorten comment about `·CancelL<`, `·CancelR<` ;…
LorenzoMolena
committed
replace `<-≤-weaken _ _ 0<1` with `0≤1` in `R₀₊CommSemiring`
LorenzoMolena
committed
move export of `PseudolatticeTheory`, add type annotation to `subtype`
LorenzoMolena
committed
add `using ()` to avoid exporting more than what is needed
LorenzoMolena
committed
update `Rationals` to use fast integers operations ; fix broken proofs in `Field.Instances.Rationals`
LorenzoMolena
committed
add instances of `Rationals` as order structures and as an `OrderedCommRing` ; add positive rationals and their properties
LorenzoMolena
committed

Commits on Apr 5, 2026

add definition of `PremetricSpace`
LorenzoMolena
committed

Commits on Apr 17, 2026

Commits on Apr 20, 2026

Commits on Apr 21, 2026