Commit 2024-06-12 14:31 e0e6e30f

View on Github →

chore: move Complex.equivRealProdAddHom earlier (#13760)

Estimated changes

Modified Mathlib/Data/Complex/Basic.lean

added def Complex.equivRealProdAddHom

added theorem Complex.equivRealProdAddHom_symm_apply

Modified Mathlib/Data/Complex/Module.lean

deleted def Complex.equivRealProdAddHom

deleted theorem Complex.equivRealProdAddHom_symm_apply