# Zulip Chat Archive

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

#### Yury G. Kudryashov (Sep 30 2020 at 12:10):

See docs#submonoid.dense_induction

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