Zulip Chat Archive
Stream: lean4
Topic: induction on quotients
Jakob von Raumer (May 17 2021 at 08:47):
The case name for induction on quotients using induction x using Quotient.ind is a, that's not really nice.
Last updated: Dec 20 2023 at 11:08 UTC