theorem ContinuousMap.norm_add_eq_max {X : Type u_1} {R : Type u_2} [TopologicalSpace X] [NormedRing R] [IsDomain R] [CompactSpace X] {f g : C(X, R)} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖