Commit 2023-08-14 12:56 cd6dd35c

View on Github →

fix: replace SMul.smul use in UpperHalfPlane (#6353)

Estimated changes

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

added def UpperHalfPlane.coe'

added theorem UpperHalfPlane.coe'_apply_complex

added theorem UpperHalfPlane.det_coe'

modified theorem UpperHalfPlane.sl_moeb

modified theorem UpperHalfPlane.subgroup_moeb

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean