Def Complex.equivRealProdAddHom

Modification history

2024-06-12 14:31

Mathlib/Data/Complex/Basic.lean

chore: move Complex.equivRealProdAddHom earlier (#13760)

Modified Complex.equivRealProdAddHom View on Github →

2023-05-02 07:59

Mathlib/Data/Complex/Module.lean

feat: port Data.Complex.Module (#3737)

Added Complex.equivRealProdAddHom View on Github →