Commit 2026-08-26 20:09 f932a30b

View on Github →

chore(Analysis/Normed/Unbundled/RingSeminorm): add missing API (#43111) This PR adds some missing API in Analysis/Normed/Unbundled/RingSeminorm.

Estimated changes

Modified Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean

added theorem AlgebraNorm.toRingNorm_apply

added theorem MulAlgebraNorm.toMulRingNorm_apply

Modified Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

deleted theorem MulRingNorm.mulRingNormEquivAbsoluteValue_apply

deleted theorem MulRingNorm.mulRingNormEquivAbsoluteValue_symm_apply

added def MulRingNorm.ofAbsoluteValue

added def MulRingNorm.toAbsoluteValue

added theorem MulRingNorm.toMulRingSeminorm_apply

added theorem RingNorm.toRingSeminorm_apply