Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 23:36 8110ab9d

View on Github →

feat(number_theory/modular): fundamental domain part 2 (#8985) This completes the argument that the standard open domain {z : |z|>1, |\Re(z)|<1/2} is a fundamental domain for the action of SL(2,\Z) on \H. The first PR (#8611) showed that every point in the upper half plane has a representative inside its closure, and here we show that representatives in the open domain are unique.

Estimated changes

added theorem abs_add'
added theorem int.one_le_abs
modified theorem int.cast_abs
added theorem int.cast_four
modified theorem int.cast_max
modified theorem int.cast_min
modified theorem int.cast_nat_abs
added theorem int.cast_one_le_of_pos
added theorem int.cast_three
deleted def modular_group.T'
added theorem modular_group.coe_S
added theorem modular_group.coe_T
modified theorem modular_group.coe_smul
modified theorem modular_group.denom_apply
modified theorem modular_group.exists_max_im
added def modular_group.fd
modified theorem modular_group.im_smul
modified theorem modular_group.neg_smul
modified theorem modular_group.re_smul
modified theorem modular_group.smul_coe