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: May 02 2025 at 03:31 UTC