Where were these lemmas moved to?

Stream: new members

[Xiang Li]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Is this related to the nat.pow change?

[Johan Commelin]

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]

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

[Xiang Li]

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]

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

[Johan Commelin]

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

[Ruben Van de Velde]

If you know the statement of the lemma, you can always library_search for the new name