Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 05:17 fe477776

View on Github →

feat(analysis/complex/upper_half_plane): new file (#8377) This file defines upper_half_plane to be the upper half plane in ℂ. We furthermore equip it with the structure of an SL(2,ℝ) action by fractional linear transformations. Co-authored by Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com Co-authored by Marc Masdeu marc.masdeu@gmail.com

Estimated changes

Created src/analysis/complex/upper_half_plane.lean

added theorem upper_half_plane.coe_im

added theorem upper_half_plane.coe_re

added theorem upper_half_plane.coe_smul

added def upper_half_plane.denom

added theorem upper_half_plane.denom_cocycle

added theorem upper_half_plane.denom_ne_zero

added def upper_half_plane.im

added theorem upper_half_plane.im_ne_zero

added theorem upper_half_plane.im_pos

added theorem upper_half_plane.im_smul

added theorem upper_half_plane.im_smul_eq_div_norm_sq

added theorem upper_half_plane.linear_ne_zero

added theorem upper_half_plane.mul_smul'

added theorem upper_half_plane.ne_zero

added theorem upper_half_plane.neg_smul

added theorem upper_half_plane.norm_sq_denom_ne_zero

added theorem upper_half_plane.norm_sq_denom_pos

added theorem upper_half_plane.norm_sq_ne_zero

added theorem upper_half_plane.norm_sq_pos

added def upper_half_plane.num

added def upper_half_plane.re

added theorem upper_half_plane.re_smul

added def upper_half_plane.smul_aux'

added theorem upper_half_plane.smul_aux'_im

added def upper_half_plane.smul_aux

added def upper_half_plane

Modified src/data/fintype/basic.lean

added theorem fintype.card_fin_even

Modified src/linear_algebra/matrix/determinant.lean

added theorem matrix.det_fin_one

added theorem matrix.det_fin_three

added theorem matrix.det_fin_two

added theorem matrix.det_fin_zero

modified theorem matrix.det_smul

Modified src/linear_algebra/special_linear_group.lean

added theorem matrix.special_linear_group.coe_neg

added theorem matrix.special_linear_group.det_ne_zero

added theorem matrix.special_linear_group.row_ne_zero