Commit 2024-04-06 09:12 7a28dbc5
View on Github →Feat (Analysis/Normed/Ring/Seminorm): add equivalence of MulRingNorms (#11852)
Include the definition of equivalence of MulRingNorms and the lemmas proving it is an equivalence relation. For this we add a new import (to Mathlib.Analysis.SpecialFunctions.Pow.Real).
We also include a lemma describing the values of a multiplicative ring norm on the naturals, stating that for all n : ℕ if f : MulRingNorm R then f n ≤ n
- 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