From 0a7ff10fcf6465406bc0734683504851c312cf81 Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Wed, 6 May 2020 16:31:27 +0000 Subject: [PATCH] feat(algebra/units): some norm_cast attributes (#2612) --- src/algebra/group/units.lean | 14 +++++++++++--- src/algebra/group_power.lean | 2 +- src/group_theory/subgroup.lean | 7 ++++--- src/group_theory/submonoid.lean | 10 ++++++---- 4 files changed, 22 insertions(+), 11 deletions(-) diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean index 580f5483d04a3..b8f83ad34e961 100644 --- a/src/algebra/group/units.lean +++ b/src/algebra/group/units.lean @@ -5,6 +5,7 @@ Authors: Kenny Lau, Mario Carneiro, Johannes, Hölzl, Chris Hughes -/ import logic.function import algebra.group.to_additive +import tactic.norm_cast /-! # Units (i.e., invertible elements) of a multiplicative monoid @@ -66,10 +67,17 @@ ext.eq_iff.symm mul_left_inv := λ u, ext u.inv_val } variables (a b : units α) {c : units α} -@[simp, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl -@[simp, to_additive] lemma coe_one : ((1 : units α) : α) = 1 := rfl +@[simp, norm_cast, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl +attribute [norm_cast] add_units.coe_add + +@[simp, norm_cast, to_additive] lemma coe_one : ((1 : units α) : α) = 1 := rfl +attribute [norm_cast] add_units.coe_zero + @[to_additive] lemma val_coe : (↑a : α) = a.val := rfl -@[to_additive] lemma coe_inv : ((a⁻¹ : units α) : α) = a.inv := rfl + +@[norm_cast, to_additive] lemma coe_inv : ((a⁻¹ : units α) : α) = a.inv := rfl +attribute [norm_cast] add_units.coe_neg + @[simp, to_additive] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _ @[simp, to_additive] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _ diff --git a/src/algebra/group_power.lean b/src/algebra/group_power.lean index a1595f9564bf4..7b3a5d2a522c6 100644 --- a/src/algebra/group_power.lean +++ b/src/algebra/group_power.lean @@ -155,7 +155,7 @@ theorem is_add_monoid_hom.map_smul (f : A → B) [is_add_monoid_hom f] (a : A) ( f (n • a) = n • f a := (add_monoid_hom.of f).map_smul a n -@[simp] lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n := +@[simp, norm_cast] lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n := (units.coe_hom M).map_pow u n end monoid diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean index b03010561674b..32d3d54169727 100644 --- a/src/group_theory/subgroup.lean +++ b/src/group_theory/subgroup.lean @@ -60,13 +60,14 @@ instance subtype.group {s : set G} [is_subgroup s] : group s := instance subtype.comm_group {G : Type*} [comm_group G] {s : set G} [is_subgroup s] : comm_group s := { .. subtype.group, .. subtype.comm_monoid } -@[simp, to_additive] +@[simp, norm_cast, to_additive] lemma is_subgroup.coe_inv {s : set G} [is_subgroup s] (a : s) : ((a⁻¹ : s) : G) = a⁻¹ := rfl +attribute [norm_cast] is_add_subgroup.coe_neg -@[simp] lemma is_subgroup.coe_gpow {s : set G} [is_subgroup s] (a : s) (n : ℤ) : ((a ^ n : s) : G) = a ^ n := +@[simp, norm_cast] lemma is_subgroup.coe_gpow {s : set G} [is_subgroup s] (a : s) (n : ℤ) : ((a ^ n : s) : G) = a ^ n := by induction n; simp [is_submonoid.coe_pow a] -@[simp] lemma is_add_subgroup.gsmul_coe {s : set A} [is_add_subgroup s] (a : s) (n : ℤ) : +@[simp, norm_cast] lemma is_add_subgroup.gsmul_coe {s : set A} [is_add_subgroup s] (a : s) (n : ℤ) : ((gsmul n a : s) : A) = gsmul n a := by induction n; simp [is_add_submonoid.smul_coe a] attribute [to_additive gsmul_coe] is_subgroup.coe_gpow diff --git a/src/group_theory/submonoid.lean b/src/group_theory/submonoid.lean index 146528158d264..69771d9893755 100644 --- a/src/group_theory/submonoid.lean +++ b/src/group_theory/submonoid.lean @@ -237,20 +237,22 @@ instance subtype.comm_monoid {M} [comm_monoid M] {s : set M} [is_submonoid s] : .. subtype.monoid } /-- Submonoids inherit the 1 of the monoid. -/ -@[simp, to_additive "An `add_submonoid` inherits the 0 of the `add_monoid`. "] +@[simp, norm_cast, to_additive "An `add_submonoid` inherits the 0 of the `add_monoid`. "] lemma is_submonoid.coe_one [is_submonoid s] : ((1 : s) : M) = 1 := rfl +attribute [norm_cast] is_add_submonoid.coe_zero /-- Submonoids inherit the multiplication of the monoid. -/ -@[simp, to_additive "An `add_submonoid` inherits the addition of the `add_monoid`. "] +@[simp, norm_cast, to_additive "An `add_submonoid` inherits the addition of the `add_monoid`. "] lemma is_submonoid.coe_mul [is_submonoid s] (a b : s) : ((a * b : s) : M) = a * b := rfl +attribute [norm_cast] is_add_submonoid.coe_add /-- Submonoids inherit the exponentiation by naturals of the monoid. -/ -@[simp] lemma is_submonoid.coe_pow [is_submonoid s] (a : s) (n : ℕ) : +@[simp, norm_cast] lemma is_submonoid.coe_pow [is_submonoid s] (a : s) (n : ℕ) : ((a ^ n : s) : M) = a ^ n := by induction n; simp [*, pow_succ] /-- An `add_submonoid` inherits the multiplication by naturals of the `add_monoid`. -/ -@[simp] lemma is_add_submonoid.smul_coe {A : Type*} [add_monoid A] {s : set A} +@[simp, norm_cast] lemma is_add_submonoid.smul_coe {A : Type*} [add_monoid A] {s : set A} [is_add_submonoid s] (a : s) (n : ℕ) : ((add_monoid.smul n a : s) : A) = add_monoid.smul n a := by {induction n, refl, simp [*, succ_smul]}