Normalize #668

kckennylau · 2019-02-01T22:13:12Z

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/normalize

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

ChrisHughes24 · 2019-02-04T16:36:51Z

Can you summarise the changes that have been made here? It takes a while to tell what is new code, and what is stuff that has just been moved.

kckennylau · 2019-02-09T22:17:15Z

old import tree: ring_theory.associated imports data.int.gcd which imports algebra.gcd_domain

new import tree: algebra.gcd_domain imports algebra.associated and data.int.gcd

moved ring_theory.associated → algebra.associated; relocated theorems about nat and int and normalization_domain to algebra.gcd_domain
made norm_unit_mul arguments implicit
defined normalize and refactor theorems with norm_unit to use normalize, including definition of gcd_domain
relocated theorems about integer being normalization domain and gcd domain from data.int.gcd to algebra.gcd_domain

ChrisHughes24 · 2019-02-09T22:42:15Z

src/algebra/gcd_domain.lean

 @[simp] theorem norm_unit_one : norm_unit (1:α) = 1 :=
 norm_unit_coe_units 1

+variables (α)


This should be implicit

But it creates metavariables which makes it impossible to use with \t.

I agree with chris. Use rw if \t gives you trouble

ChrisHughes24 · 2019-02-09T22:43:50Z

src/algebra/gcd_domain.lean

+
+@[simp] lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x :=
+⟨λ hx, is_unit_iff_exists_inv.2 ⟨_, hx⟩, λ ⟨u, hu⟩, hu.symm ▸ normalize_coe_units u⟩
+


debatable whether this should be simp. Equalities are good.

ChrisHughes24 · 2019-02-09T22:44:59Z

src/algebra/gcd_domain.lean

+
+lemma normalize_nat_coe (n : ℕ) : normalize (n : ℤ) = n :=
+normalize_of_nonneg (coe_nat_le_coe_nat_of_le $ nat.zero_le n)
+


normalize_coe_nat

ChrisHughes24 · 2019-02-09T22:52:12Z

src/ring_theory/multiplicity.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Chris Hughes
 -/
-import data.nat.enat ring_theory.associated
+import algebra.gcd_domain data.nat.enat


Does this use anything from gcd_domain or is a weaker import possible?

digama0 · 2019-02-09T23:23:30Z

src/algebra/gcd_domain.lean

  calc a * ↑(norm_unit a) = a * ↑(norm_unit a) * ↑u * ↑u⁻¹:
      (units.mul_inv_cancel_right _ _).symm
    ... = a * ↑u * ↑(norm_unit a) * ↑u⁻¹ : by rw mul_right_comm a
 end

-theorem dvd_antisymm_of_norm {a b : α}
-  (ha : norm_unit a = 1) (hb : norm_unit b = 1) (hab : a ∣ b) (hba : b ∣ a) :
+@[simp] lemma normalize_eq_normalize_iff {x y : α} : normalize x = normalize y ↔ x ∣ y ∧ y ∣ x :=


this doesn't look like it should be a simp lemma either

kckennylau · 2019-02-10T20:22:48Z

Updated summary: I just added normalize x to replace x * norm_unit x, including in the definition of gcd_domain.

kckennylau assigned ChrisHughes24 Feb 1, 2019

kckennylau requested a review from ChrisHughes24 February 1, 2019 22:13

cipher1024 force-pushed the master branch 2 times, most recently from f623d34 to 1ed7ad1 Compare February 8, 2019 12:35

ChrisHughes24 reviewed Feb 9, 2019

View reviewed changes

digama0 reviewed Feb 9, 2019

View reviewed changes

kckennylau force-pushed the normalize branch 2 times, most recently from 0b62a9b to 14e360e Compare February 10, 2019 14:31

kckennylau closed this Feb 10, 2019

feat(algebra/gcd_domain): normalize

5bf83a0

kckennylau reopened this Feb 10, 2019

kckennylau force-pushed the normalize branch from 14e360e to 5bf83a0 Compare February 10, 2019 20:20

ChrisHughes24 merged commit 091cad7 into master Feb 10, 2019

ChrisHughes24 deleted the normalize branch February 10, 2019 21:50

cipher1024 pushed a commit that referenced this pull request Feb 12, 2019

feat(algebra/gcd_domain): normalize (#668)

88913e1

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Normalize #668

Normalize #668

kckennylau commented Feb 1, 2019

ChrisHughes24 commented Feb 4, 2019

kckennylau commented Feb 9, 2019

ChrisHughes24 Feb 9, 2019

kckennylau Feb 9, 2019 •

edited

digama0 Feb 9, 2019

kckennylau Feb 10, 2019

ChrisHughes24 Feb 9, 2019

kckennylau Feb 10, 2019

ChrisHughes24 Feb 9, 2019

kckennylau Feb 10, 2019

ChrisHughes24 Feb 9, 2019

kckennylau Feb 10, 2019

digama0 Feb 9, 2019

kckennylau Feb 10, 2019

kckennylau commented Feb 10, 2019


		@[simp] lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x :=
		⟨λ hx, is_unit_iff_exists_inv.2 ⟨_, hx⟩, λ ⟨u, hu⟩, hu.symm ▸ normalize_coe_units u⟩


		lemma normalize_nat_coe (n : ℕ) : normalize (n : ℤ) = n :=
		normalize_of_nonneg (coe_nat_le_coe_nat_of_le $ nat.zero_le n)

Normalize #668

Normalize #668

Conversation

kckennylau commented Feb 1, 2019

ChrisHughes24 commented Feb 4, 2019

kckennylau commented Feb 9, 2019

Choose a reason for hiding this comment

kckennylau Feb 9, 2019 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kckennylau commented Feb 10, 2019

kckennylau Feb 9, 2019 •

edited