Commit 2024-09-04 05:09 9f572fca

View on Github →

feat: Conjugation-negation operator (#16181) This is a fundamental operator in discrete Fourier analysis. For example, it is the operator relating convolution and difference convolution: https://yaeldillies.github.io/LeanAPAP/docs/LeanAPAP/Prereqs/Convolution/Discrete/Defs.html#conv_conjneg From LeanAPAP

Estimated changes

added theorem conjneg_neg'
added theorem conjneg_nonneg
added theorem conjneg_nonpos
added theorem conjneg_pos
added def conjneg
added def conjnegRingHom
added theorem conjneg_add
added theorem conjneg_apply
added theorem conjneg_bijective
added theorem conjneg_conj
added theorem conjneg_conjneg
added theorem conjneg_eq_one
added theorem conjneg_eq_zero
added theorem conjneg_inj
added theorem conjneg_injective
added theorem conjneg_involutive
added theorem conjneg_mul
added theorem conjneg_ne_conjneg
added theorem conjneg_ne_one
added theorem conjneg_ne_zero
added theorem conjneg_neg
added theorem conjneg_one
added theorem conjneg_prod
added theorem conjneg_sub
added theorem conjneg_sum
added theorem conjneg_surjective
added theorem conjneg_zero
added theorem sum_conjneg
added theorem support_conjneg