Commit 2023-04-17 08:52 2313f45b

View on Github →

feat: port Analysis.Normed.Ring.Seminorm (#3211) ~~This is currently stuck on an issue as indicated in line 111.~~ edit: fixed by the etaExperiment option

Estimated changes

Modified Mathlib.lean

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

added theorem MulRingNorm.apply_one

added theorem MulRingNorm.ext

added structure MulRingNorm

added theorem MulRingSeminorm.apply_one

added theorem MulRingSeminorm.ext

added theorem MulRingSeminorm.toFun_eq_coe

added structure MulRingSeminorm

added theorem RingNorm.apply_one

added theorem RingNorm.ext

added structure RingNorm

added theorem RingSeminorm.apply_one

added theorem RingSeminorm.eq_zero_iff

added theorem RingSeminorm.ext

added theorem RingSeminorm.ne_zero_iff

added theorem RingSeminorm.seminorm_one_eq_one_iff_ne_zero

added theorem RingSeminorm.toFun_eq_coe

added def RingSeminorm.toRingNorm

added structure RingSeminorm

added def normRingNorm

added def normRingSeminorm