## Stream: new members

### Topic: Word in reduced form

#### Giacomo Maletto (Nov 16 2021 at 21:18):

Suppose I'm working with an element of free_group α and I want to express "let $v = v_1^{\epsilon_1} \dots v_k^{\epsilon_k}$ be its reduced form". If α has decidable_eq I think I can use the reduce function together with theorem reduce.self, but is it possible to prove a general statement like "a word always admits reduced form"?

#### David Wärn (Nov 16 2021 at 21:25):

Yes, every type has decidable equality if you're working classically

#### Reid Barton (Nov 16 2021 at 21:26):

And if every word has a reduced form then α must have decidable equality, because given $x$ and $y$ you can look at the reduced form of $xy^{-1}$ to decide whether $x = y$

#### Giacomo Maletto (Nov 16 2021 at 21:28):

Interesting, and how do you tell Lean that every type has decidable equality?

#### Giacomo Maletto (Nov 16 2021 at 21:30):

That is to say, how can I use that fact in a proof?

#### Kevin Buzzard (Nov 16 2021 at 21:36):

Use the classical tactic in your proof

Last updated: Dec 20 2023 at 11:08 UTC