# Zulip Chat Archive

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