Def RingHom.IsBounded

Modification history

2025-03-09 23:03
Mathlib/Analysis/Normed/Field/Basic.lean
refactor(Mathlib/Analysis/Normed): disentangle normed rings and normed fields (#22744) …
Modified RingHom.IsBoundedView on Github →
2024-10-02 17:07
Mathlib/Analysis/Normed/Field/Basic.lean
feat(Analysis.Normed.Ring.IsPowMulFaithful): prove eq_of_powMul_faithful (#15445) …
Added RingHom.IsBoundedView on Github →