Commit 2024-07-30 11:18 0f83d879

View on Github →

feat(Analysis.Normed.Ring.SeminormFromConst): add seminormFromConst (#14361) We prove [BGR, Proposition 1.3.2/2] : starting from a power-multiplicative seminorm on a commutative ring R and a nonzero c : R, we create a new power-multiplicative seminorm for which c is multiplicative.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean

added def normFromConst

added def seminormFromConst'

added def seminormFromConst

added theorem seminormFromConstRingNormOfField_def

added theorem seminormFromConst_apply_c

added theorem seminormFromConst_apply_of_isMul

added theorem seminormFromConst_bddBelow

added theorem seminormFromConst_const_mul

added theorem seminormFromConst_def

added theorem seminormFromConst_isLimit

added theorem seminormFromConst_isMul_of_isMul

added theorem seminormFromConst_isNonarchimedean

added theorem seminormFromConst_isPowMul

added theorem seminormFromConst_le_seminorm

added theorem seminormFromConst_one

added theorem seminormFromConst_one_le

added def seminormFromConst_seq

added theorem seminormFromConst_seq_antitone

added theorem seminormFromConst_seq_def

added theorem seminormFromConst_seq_nonneg

added theorem seminormFromConst_seq_one

added theorem seminormFromConst_seq_zero

Modified Mathlib/Data/Real/Basic.lean

modified def IsNonarchimedean

added def IsPowMul