# Zulip Chat Archive

## Stream: new members

### Topic: Where were these lemmas moved to?

#### Xiang Li (Oct 31 2020 at 08:42):

I have difficult finding out two lemmas called map_mul_of_map_pow_two and ring_hom.mk_mul_self_of_two_ne_zero because their name were changed. Is there any way tackle this kind of problem?

#### Johan Commelin (Oct 31 2020 at 08:46):

Do you know in which file they used to be? (Or a commit that still contained them?)

#### Johan Commelin (Oct 31 2020 at 08:46):

I just searched through the commit logs, and they don't mention their removal, which is unfortunate.

#### Johan Commelin (Oct 31 2020 at 08:47):

Is this related to the `nat.pow`

change?

#### Johan Commelin (Oct 31 2020 at 08:48):

```
commit d8707432c03714519d7127016341d820c3c30cf6
Author: Alex J. Best <alex.j.best@gmail.com>
Date: Fri Jul 17 14:04:32 2020 -0400
begin moving
diff --git a/src/field_theory/complete_ordered.lean b/src/field_theory/complete_ordered.lean
index a0e737616..d79ec1506 100644
--- a/src/field_theory/complete_ordered.lean
+++ b/src/field_theory/complete_ordered.lean
@@ -23,6 +23,7 @@ We introduce definitions of Conditionally complete linear ordered fields, show a
archimedean, and define equivalences between these fields. We also construct the natural map from a
`linear_ordered_field` to such a field.
+As a proof outline this follows:
https://mathoverflow.net/questions/362991/who-first-characterized-the-real-numbers-as-the-unique-complete-ordered-field
## Tags
@@ -32,19 +33,6 @@ reals, conditionally complete, ordered field
noncomputable theory
open_locale classical
-lemma map_mul_of_map_pow_two (R S : Type*) [comm_ring R] [integral_domain S] (h2 : (2 : S) ≠ 0)
- (f : R →+ S) (h : ∀ x, f (x * x) = f x * f x) (x y : R) : f (x * y) = f x * f y :=
-begin
- have hxy := h (x + y),
- simp only [mul_add, add_mul, h x, h y, f.map_add] at hxy,
- rw [← sub_eq_zero_iff_eq] at hxy,
- ring at hxy,
- rw [mul_comm y x, mul_assoc, mul_comm (f y)] at hxy,
- rw [← two_mul, add_comm, ← sub_eq_add_neg, ← mul_sub, mul_eq_zero, sub_eq_zero_iff_eq] at hxy,
- rw classical.or_iff_not_imp_left at hxy,
- exact hxy h2,
-end
```

#### Johan Commelin (Oct 31 2020 at 08:49):

Hmm, sorry, that's not a commit on master

#### Xiang Li (Oct 31 2020 at 08:51):

Thank you very much! I am reading some code he wrote and thought their names were changed. What's your way to search these?

#### Johan Commelin (Oct 31 2020 at 08:54):

Aah right... I was really confused, because I couldn't find any commit on master that mentioned this.

#### Johan Commelin (Oct 31 2020 at 08:54):

```
git log -p --all -G "map_mul_of_map_pow_two"
```

#### Ruben Van de Velde (Oct 31 2020 at 09:39):

If you know the statement of the lemma, you can always `library_search`

for the new name

Last updated: Dec 20 2023 at 11:08 UTC