Induction over a generating set

Stream: Is there code for X?

[Eric Wieser]

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]

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]

See docs#submonoid.dense_induction

[Patrick Massot]

I don't think using "dense" is a good idea here. I think "generating" would be clearer.

[Eric Wieser]

Is there an equivalent for subrings and subalgebras?

[Eric Wieser]

docs#subring.closure_induction

[Sebastien Gouezel]

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 s.

[Eric Wieser]

Should dense_induction be renamed to closure_induction to match?

[Eric Wieser]

Nevermind, I see that docs#submonoid.closure_induction already exists