## Stream: Is there code for X?

### Topic: Induction over a generating set

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

#### 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):

docs#subring.closure_induction

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

#### Eric Wieser (Sep 30 2020 at 13:55):

Should 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