Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace without_zero_le_one #16525

Closed
wants to merge 9 commits into from

Merge branch 'master' into FR_order_refactor18

9c0bf19
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Closed

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace without_zero_le_one #16525

Merge branch 'master' into FR_order_refactor18
9c0bf19
Select commit
Loading
Failed to load commit list.

Annotations

5 warnings
build
succeeded Mar 23, 2024 in 4s