Zulip Chat Archive

Stream: new members

Topic: Where were these lemmas moved to?


view this post on Zulip 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?

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 31 2020 at 08:47):

Is this related to the nat.pow change?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 31 2020 at 08:49):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 31 2020 at 08:54):

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

view this post on Zulip 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: May 06 2021 at 21:09 UTC