Commit 2024-08-13 09:26 4c9b452c

View on Github →

refactor: Make circle a type Circle (#15116) See https://github.com/leanprover-community/mathlib4/wiki/Tradeoffs-of-concrete-types-defined-as-subobjects for context

Estimated changes

added theorem Circle.abs_coe
added def Circle.coeHom
added theorem Circle.coe_div
added theorem Circle.coe_inv
added theorem Circle.coe_inv_eq_conj
added theorem Circle.coe_mul
added theorem Circle.coe_ne_zero
added theorem Circle.coe_one
added def Circle.exp
added def Circle.expHom
added theorem Circle.exp_add
added theorem Circle.exp_apply
added theorem Circle.exp_neg
added theorem Circle.exp_sub
added theorem Circle.exp_zero
added theorem Circle.normSq_coe
added theorem Circle.smul_def
added def Circle.toUnits
added theorem Circle.toUnits_apply
added def Circle
deleted theorem abs_coe_circle
deleted def circle.toUnits
deleted theorem circle.toUnits_apply
deleted theorem circle_def
deleted theorem coe_div_circle
deleted theorem coe_inv_circle
deleted theorem coe_inv_circle_eq_conj
deleted def expMapCircle
deleted def expMapCircleHom
deleted theorem expMapCircle_add
deleted theorem expMapCircle_apply
deleted theorem expMapCircle_neg
deleted theorem expMapCircle_sub
deleted theorem expMapCircle_zero
modified theorem mem_circle_iff_normSq
deleted theorem ne_zero_of_mem_circle
deleted theorem normSq_eq_of_mem_circle
deleted theorem norm_circle_smul
modified theorem det_rotation
modified theorem linearEquiv_det_rotation
modified def rotation
modified def rotationOf
modified theorem rotationOf_rotation
modified theorem rotation_apply
modified theorem rotation_ne_conjLIE
modified theorem rotation_symm
modified theorem rotation_trans
modified theorem toMatrix_rotation
modified theorem Real.continuous_fourierChar
modified theorem AddCircle.toCircle_apply_mk
added theorem Circle.arg_eq_arg
added theorem Circle.arg_exp
added theorem Circle.exp_add_two_pi
added theorem Circle.exp_arg
added theorem Circle.exp_eq_exp
added theorem Circle.exp_sub_two_pi
added theorem Circle.exp_two_pi
added theorem Circle.injective_arg
added theorem Circle.invOn_arg_exp
added theorem Circle.periodic_exp
deleted theorem arg_expMapCircle
deleted theorem circle.arg_eq_arg
deleted theorem circle.injective_arg
deleted theorem expMapCircle_add_two_pi
deleted theorem expMapCircle_arg
deleted theorem expMapCircle_sub_two_pi
deleted theorem expMapCircle_two_pi
deleted theorem invOn_arg_expMapCircle
deleted theorem periodic_expMapCircle
modified theorem ZMod.injective_toCircle
added theorem contMDiff_circleExp
deleted theorem contMDiff_expMapCircle