From 5a835b7bcd7934dd93bef973d974f5475e4be4a5 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 15 Dec 2021 21:49:21 +0000 Subject: [PATCH] chore(*): tweaks taken from gh-8889 (#10829) That PR is stale, but contained some trivial changes we should just take. --- src/analysis/complex/circle.lean | 1 + src/group_theory/quotient_group.lean | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/analysis/complex/circle.lean b/src/analysis/complex/circle.lean index da36d03cc2345..2535180ffee8b 100644 --- a/src/analysis/complex/circle.lean +++ b/src/analysis/complex/circle.lean @@ -102,6 +102,7 @@ subtype.ext $ by simp only [exp_map_circle_apply, submonoid.coe_mul, of_real_add /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`, considered as a homomorphism of groups. -/ +@[simps] def exp_map_circle_hom : ℝ →+ (additive circle) := { to_fun := additive.of_mul ∘ exp_map_circle, map_zero' := exp_map_circle_zero, diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean index 82a2d6a406351..2ef654eff4ed5 100644 --- a/src/group_theory/quotient_group.lean +++ b/src/group_theory/quotient_group.lean @@ -124,10 +124,12 @@ lemma coe_inv (a : G) : ((a⁻¹ : G) : Q) = a⁻¹ := rfl @[simp, to_additive quotient_add_group.coe_sub] lemma coe_div (a b : G) : ((a / b : G) : Q) = a / b := by simp [div_eq_mul_inv] -@[simp] lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := +@[simp, to_additive quotient_add_group.coe_nsmul] +lemma coe_pow (a : G) (n : ℕ) : ((a ^ n : G) : Q) = a ^ n := (mk' N).map_pow a n -@[simp] lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := +@[simp, to_additive quotient_add_group.coe_zsmul] +lemma coe_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = a ^ n := (mk' N).map_zpow a n /-- A group homomorphism `φ : G →* H` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a