Stream: Is there code for X?
Eric Wieser (Sep 30 2020 at 11:15):
If I have can show that
sx is a generating set of a monoid
X, is there an induction principle that can take something like
∀ x ∈ sx, p x,
p 1, and
∀ x y, p x → p y → p (x * y) to produce
∀ x, p x? (and the same for algebras, rings, etc...)
Eric Wieser (Sep 30 2020 at 11:18):
I ended up building one myself for a special case in #4335, but the approach strikes me as obviously generalizable, and therefore likely to already exist.
Yury G. Kudryashov (Sep 30 2020 at 12:10):
Patrick Massot (Sep 30 2020 at 13:39):
I don't think using "dense" is a good idea here. I think "generating" would be clearer.
Eric Wieser (Sep 30 2020 at 13:47):
Is there an equivalent for subrings and subalgebras?
Eric Wieser (Sep 30 2020 at 13:50):
Sebastien Gouezel (Sep 30 2020 at 13:51):
Also, the assumption is a little bit too strong, in
∀ (x y : M), p x → p y → p (x * y) one could also require that
x belongs to
Eric Wieser (Sep 30 2020 at 13:55):
dense_induction be renamed to
closure_induction to match?
Eric Wieser (Sep 30 2020 at 13:57):
Nevermind, I see that docs#submonoid.closure_induction already exists
Last updated: May 07 2021 at 19:12 UTC