Commit 2024-10-19 16:03 e06fe3e8

View on Github →

chore: do not use · ≈ · in Quotient.mk_out (#17940)

Estimated changes

modified theorem Quotient.mk_out