Commit 2022-11-10 23:34 8983526d
View on Github →feat: port Data.Quot (#559)
This is my first PR to mathlib4 so please check carefully!
This PR ports data.quot
and the definition of eqv_gen
from core Lean 3.
feat: port Data.Quot (#559)
This is my first PR to mathlib4 so please check carefully!
This PR ports data.quot
and the definition of eqv_gen
from core Lean 3.