Commit 2023-06-28 11:45 af3e121c

View on Github →

feat: port NumberTheory.Modular (#5540)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Modular.lean

added theorem ModularGroup.abs_c_le_one

added theorem ModularGroup.abs_two_mul_re_lt_one_of_mem_fdo

added theorem ModularGroup.bottom_row_coprime

added theorem ModularGroup.bottom_row_surj

added theorem ModularGroup.c_eq_zero

added theorem ModularGroup.coe_T_zpow_smul_eq

added theorem ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo

added theorem ModularGroup.eq_zero_of_mem_fdo_of_T_zpow_mem_fdo

added theorem ModularGroup.exists_eq_T_zpow_of_c_eq_zero

added theorem ModularGroup.exists_max_im

added theorem ModularGroup.exists_row_one_eq_and_min_re

added theorem ModularGroup.exists_smul_mem_fd

added def ModularGroup.fd

added def ModularGroup.fdo

added theorem ModularGroup.g_eq_of_c_eq_one

added theorem ModularGroup.im_T_inv_smul

added theorem ModularGroup.im_T_smul

added theorem ModularGroup.im_T_zpow_smul

added theorem ModularGroup.im_lt_im_S_smul

added def ModularGroup.lcRow0

added def ModularGroup.lcRow0Extend

added theorem ModularGroup.lcRow0_apply

added theorem ModularGroup.normSq_S_smul_lt_one

added theorem ModularGroup.one_lt_normSq_T_zpow_smul

added theorem ModularGroup.re_T_inv_smul

added theorem ModularGroup.re_T_smul

added theorem ModularGroup.re_T_zpow_smul

added theorem ModularGroup.smul_eq_lcRow0_add

added theorem ModularGroup.tendsto_abs_re_smul

added theorem ModularGroup.tendsto_lcRow0

added theorem ModularGroup.tendsto_normSq_coprime_pair

added theorem ModularGroup.three_lt_four_mul_im_sq_of_mem_fdo