Structures · Algebra

RingNormClass

RingNormClass F α states that F is a type of β-valued norms on the ring α. You should extend this class when you extend RingNorm.

Defined in

Mathlib.Algebra.Order.Hom.Basic

Shape

3 explicit arguments · adds eq_zero_of_map_eq_zero