Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_R_or_C.conj_mul

Modification history

2023-05-05 01:40
src/data/is_R_or_C/basic.lean
chore(data/is_R_or_C/basic): rename `conj_mul_eq_norm_sq_left` to `conj_mul` (#18939)
Added is_R_or_C.conj_mulView on Github →