Commit 2024-06-12 07:57 d085ccc9
View on Github →Feat (Analysis/Normed/Ring/Seminorm): add lemmas on equivalence of MulRingNorms (#12517)
Include the following lemmas on equivalence of MulRingNorms.
lemma f_of_abs_eq_f (x : ℤ) : f (Int.natAbs x) = f x
lemma NormRat_eq_on_Int_iff_eq_on_Nat : (∀ n : ℕ , f n = g n) ↔ (∀ n : ℤ , f n = g n)
lemma NormRat_eq_iff_eq_on_Nat : (∀ n : ℕ , f n = g n) ↔ f = g
lemma NormRat_equiv_iff_equiv_on_Nat : (∃ c : ℝ, 0 < c ∧ (∀ n : ℕ , (f n)^c = g n)) ↔ f.equiv g
David Kurniadi Angdinata dka31@cantab.ac.uk Fabrizio Barroero fabrizio.barroero@uniroma3.it Laura Capuano laura.capuano@uniroma3.it Nirvana Coppola nirvanac93@gmail.com María Inés de Frutos Fernández maria.defrutos@uam.es Silvain Rideau-Kikuchi silvain.rideau-kikuchi@ens.fr Sam van Gool vangool@irif.fr Francesco Veneziano veneziano@dima.unige.it