Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-05 01:40 25580801

View on Github →

chore(data/is_R_or_C/basic): rename conj_mul_eq_norm_sq_left to conj_mul (#18939)

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

Modified src/analysis/normed_space/extend.lean

Modified src/data/is_R_or_C/basic.lean

added theorem is_R_or_C.conj_mul

deleted theorem is_R_or_C.conj_mul_eq_norm_sq_left

Modified src/topology/continuous_function/ideals.lean