Commit 2022-10-11 18:36 93def16e

View on Github →

feat(analysis/normed/ring/seminorm): Multiplicative ring norms (#16766) Define mul_ring_seminorm/mul_ring_norm, the type of multiplicative ring_seminorm/ring_norm.

Estimated changes

Modified src/analysis/normed/ring/seminorm.lean

added theorem mul_ring_norm.apply_one

added theorem mul_ring_norm.ext

added theorem mul_ring_norm.to_fun_eq_coe

added structure mul_ring_norm

added theorem mul_ring_seminorm.apply_one

added theorem mul_ring_seminorm.ext

added theorem mul_ring_seminorm.to_fun_eq_coe

added structure mul_ring_seminorm

modified structure ring_norm

modified structure ring_seminorm