diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean index a77592630feab..04390ac4239de 100644 --- a/archive/sensitivity.lean +++ b/archive/sensitivity.lean @@ -28,8 +28,8 @@ by Leonardo de Moura at Microsoft Research, and his collaborators and using Lean's user maintained mathematics library (https://github.com/leanprover-community/mathlib). -The project was developed at https://github.com/leanprover-community/lean-sensitivity -and is now archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean +The project was developed at https://github.com/leanprover-community/lean-sensitivity and is now +archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean -/ /-! The next two lines assert we do not want to give a constructive proof, @@ -177,7 +177,8 @@ noncomputable def e : Π {n}, Q n → V n /-- The dual basis to `e`, defined inductively. -/ noncomputable def ε : Π {n : ℕ} (p : Q n), V n →ₗ[ℝ] ℝ | 0 _ := linear_map.id -| (n+1) p := cond (p 0) ((ε $ π p).comp $ linear_map.fst _ _ _) ((ε $ π p).comp $ linear_map.snd _ _ _) +| (n+1) p := cond (p 0) ((ε $ π p).comp $ linear_map.fst _ _ _) + ((ε $ π p).comp $ linear_map.snd _ _ _) variable {n : ℕ} @@ -211,7 +212,8 @@ begin let q : Q (n+1) := λ i, if h : i = 0 then ff else p (i.pred h)], all_goals { specialize h q, - rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|> rw [ε, show q 0 = ff, from rfl, cond_ff] at h, + rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|> + rw [ε, show q 0 = ff, from rfl, cond_ff] at h, rwa show p = π q, by { ext, simp [q, fin.succ_ne_zero, π] } } } end diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index 4ed22bd8eab62..0f00ea99fd800 100644 --- a/src/algebra/algebra/basic.lean +++ b/src/algebra/algebra/basic.lean @@ -121,7 +121,8 @@ it suffices to check the `algebra_map`s agree. -- We'll later use this to show `algebra ℤ M` is a subsingleton. @[ext] lemma algebra_ext {R : Type*} [comm_semiring R] {A : Type*} [semiring A] (P Q : algebra R A) - (w : ∀ (r : R), by { haveI := P, exact algebra_map R A r } = by { haveI := Q, exact algebra_map R A r }) : + (w : ∀ (r : R), by { haveI := P, exact algebra_map R A r } = + by { haveI := Q, exact algebra_map R A r }) : P = Q := begin unfreezingI { rcases P with ⟨⟨P⟩⟩, rcases Q with ⟨⟨Q⟩⟩ }, @@ -699,7 +700,8 @@ by { ext, simp } by { ext, simp } /-- If an algebra morphism has an inverse, it is a algebra isomorphism. -/ -def of_alg_hom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂) (h₂ : g.comp f = alg_hom.id R A₁) : A₁ ≃ₐ[R] A₂ := +def of_alg_hom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂) + (h₂ : g.comp f = alg_hom.id R A₁) : A₁ ≃ₐ[R] A₂ := { inv_fun := g, left_inv := alg_hom.ext_iff.1 h₂, right_inv := alg_hom.ext_iff.1 h₁, @@ -799,8 +801,8 @@ include R S A Other than that, `algebra.comap` is now deprecated and replaced with `is_scalar_tower`. -/ /- This is done to avoid a type class search with meta-variables `algebra R ?m_1` and `algebra ?m_1 A -/ -/- The `nolint` attribute is added because it has unused arguments `R` and `S`, but these are necessary for synthesizing the - appropriate type classes -/ +/- The `nolint` attribute is added because it has unused arguments `R` and `S`, but these are + necessary for synthesizing the appropriate type classes -/ @[nolint unused_arguments] def comap : Type w := A diff --git a/src/algebra/algebra/operations.lean b/src/algebra/algebra/operations.lean index 080c9ad08b1cd..21a142b2763f8 100644 --- a/src/algebra/algebra/operations.lean +++ b/src/algebra/algebra/operations.lean @@ -17,7 +17,8 @@ Let `R` be a commutative ring (or semiring) and aet `A` be an `R`-algebra. * `1 : submodule R A` : the R-submodule R of the R-algebra A * `has_mul (submodule R A)` : multiplication of two sub-R-modules M and N of A is defined to be the smallest submodule containing all the products `m * n`. -* `has_div (submodule R A)` : `I / J` is defined to be the submodule consisting of all `a : A` such that `a • J ⊆ I` +* `has_div (submodule R A)` : `I / J` is defined to be the submodule consisting of all `a : A` such + that `a • J ⊆ I` It is proved that `submodule R A` is a semiring, and also an algebra over `set A`. @@ -189,7 +190,8 @@ begin apply mul_subset_mul } end -/-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets on either side). -/ +/-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets +on either side). -/ def span.ring_hom : set_semiring A →+* submodule R A := { to_fun := submodule.span R, map_zero' := span_empty, diff --git a/src/algebra/archimedean.lean b/src/algebra/archimedean.lean index 5887a1a4740e2..9c0a2b7ea03f6 100644 --- a/src/algebra/archimedean.lean +++ b/src/algebra/archimedean.lean @@ -18,8 +18,8 @@ class archimedean (α) [ordered_add_comm_monoid α] : Prop := namespace decidable_linear_ordered_add_comm_group variables [decidable_linear_ordered_add_comm_group α] [archimedean α] -/-- An archimedean decidable linearly ordered `add_comm_group` has a version of the floor: for `a > 0`, -any `g` in the group lies between some two consecutive multiples of `a`. -/ +/-- An archimedean decidable linearly ordered `add_comm_group` has a version of the floor: for +`a > 0`, any `g` in the group lies between some two consecutive multiples of `a`. -/ lemma exists_int_smul_near_of_pos {a : α} (ha : 0 < a) (g : α) : ∃ k, k •ℤ a ≤ g ∧ g < (k + 1) •ℤ a := begin @@ -167,8 +167,8 @@ instance : archimedean ℕ := instance : archimedean ℤ := ⟨λ n m m0, ⟨n.to_nat, le_trans (int.le_to_nat _) $ -by simpa only [nsmul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one] using mul_le_mul_of_nonneg_left - (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩ +by simpa only [nsmul_eq_mul, int.nat_cast_eq_coe_nat, zero_add, mul_one] + using mul_le_mul_of_nonneg_left (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat)⟩⟩ /-- A linear ordered archimedean ring is a floor ring. This is not an `instance` because in some cases we have a computable `floor` function. -/ diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean index e715514a378f8..b9a06ae370c0c 100644 --- a/src/algebra/associated.lean +++ b/src/algebra/associated.lean @@ -164,7 +164,8 @@ begin exact H _ o.1 _ o.2 h.symm end -lemma irreducible_of_prime [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) : irreducible p := +lemma irreducible_of_prime [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) : + irreducible p := ⟨hp.not_unit, λ a b hab, (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.div_or_div (hab ▸ (dvd_refl _))).elim (λ ⟨x, hx⟩, or.inr (is_unit_iff_dvd_one.2 @@ -298,7 +299,8 @@ lemma eq_zero_iff_of_associated [comm_monoid_with_zero α] {a b : α} (h : a ~ lemma ne_zero_iff_of_associated [comm_monoid_with_zero α] {a b : α} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0 := by haveI := classical.dec; exact not_iff_not.2 (eq_zero_iff_of_associated h) -lemma prime_of_associated [comm_monoid_with_zero α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : prime q := +lemma prime_of_associated [comm_monoid_with_zero α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : + prime q := ⟨(ne_zero_iff_of_associated h).1 hp.ne_zero, let ⟨u, hu⟩ := h in ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩, diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean index b5a7b2df3867f..410a55c04a59d 100644 --- a/src/algebra/big_operators/basic.lean +++ b/src/algebra/big_operators/basic.lean @@ -122,7 +122,8 @@ lemma ring_hom.map_multiset_sum [semiring β] [semiring γ] (f : β →+* γ) (s f s.sum = (s.map f).sum := f.to_add_monoid_hom.map_multiset_sum s -lemma ring_hom.map_prod [comm_semiring β] [comm_semiring γ] (g : β →+* γ) (f : α → β) (s : finset α) : +lemma ring_hom.map_prod [comm_semiring β] [comm_semiring γ] (g : β →+* γ) (f : α → β) + (s : finset α) : g (∏ x in s, f x) = ∏ x in s, g (f x) := g.to_monoid_hom.map_prod f s diff --git a/src/algebra/big_operators/intervals.lean b/src/algebra/big_operators/intervals.lean index 9f48df78995cb..8aede9d22b545 100644 --- a/src/algebra/big_operators/intervals.lean +++ b/src/algebra/big_operators/intervals.lean @@ -20,7 +20,8 @@ open_locale big_operators nat namespace finset -variables {α : Type u} {β : Type v} {γ : Type w} {s₂ s₁ s : finset α} {a : α} {g f : α → β} [comm_monoid β] +variables {α : Type u} {β : Type v} {γ : Type w} {s₂ s₁ s : finset α} {a : α} {g f : α → β} + [comm_monoid β] lemma sum_Ico_add {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (m n k : ℕ) : (∑ l in Ico m n, f (k + l)) = (∑ l in Ico (m + k) (n + k), f l) := diff --git a/src/algebra/big_operators/ring.lean b/src/algebra/big_operators/ring.lean index c763dd2de3278..5ca9d711fa7d7 100644 --- a/src/algebra/big_operators/ring.lean +++ b/src/algebra/big_operators/ring.lean @@ -153,7 +153,8 @@ end comm_semiring /-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets of `s`, and over all subsets of `s` to which one adds `x`. -/ @[to_additive] -lemma prod_powerset_insert [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x ∉ s) (f : finset α → β) : +lemma prod_powerset_insert [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x ∉ s) + (f : finset α → β) : (∏ a in (insert x s).powerset, f a) = (∏ a in s.powerset, f a) * (∏ t in s.powerset, f (insert x t)) := begin diff --git a/src/algebra/category/Algebra/basic.lean b/src/algebra/category/Algebra/basic.lean index c307a23c7f66b..5aef979c8b944 100644 --- a/src/algebra/category/Algebra/basic.lean +++ b/src/algebra/category/Algebra/basic.lean @@ -48,7 +48,8 @@ instance has_forget_to_Module : has_forget₂ (Algebra R) (Module R) := { obj := λ M, Module.of R M, map := λ M₁ M₂ f, alg_hom.to_linear_map f, } } -/-- The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. -/ +/-- The object in the category of R-algebras associated to a type equipped with the appropriate +typeclasses. -/ def of (X : Type v) [ring X] [algebra R X] : Algebra R := ⟨X⟩ instance : inhabited (Algebra R) := ⟨of R R⟩ @@ -58,7 +59,8 @@ lemma coe_of (X : Type u) [ring X] [algebra R X] : (of R X : Type u) = X := rfl variables {R} -/-- Forgetting to the underlying type and then building the bundled object returns the original algebra. -/ +/-- Forgetting to the underlying type and then building the bundled object returns the original +algebra. -/ @[simps] def of_self_iso (M : Algebra R) : Algebra.of R M ≅ M := { hom := 𝟙 M, inv := 𝟙 M } @@ -122,7 +124,8 @@ def to_alg_equiv {X Y : Algebra R} (i : X ≅ Y) : X ≃ₐ[R] Y := end category_theory.iso -/-- algebra equivalences between `algebras`s are the same as (isomorphic to) isomorphisms in `Algebra` -/ +/-- Algebra equivalences between `algebras`s are the same as (isomorphic to) isomorphisms in +`Algebra`. -/ @[simps] def alg_equiv_iso_Algebra_iso {X Y : Type u} [ring X] [ring Y] [algebra R X] [algebra R Y] : diff --git a/src/algebra/category/CommRing/adjunctions.lean b/src/algebra/category/CommRing/adjunctions.lean index 39797e76a0c23..1dffdd71b5c9d 100644 --- a/src/algebra/category/CommRing/adjunctions.lean +++ b/src/algebra/category/CommRing/adjunctions.lean @@ -30,7 +30,8 @@ def free : Type u ⥤ CommRing := { obj := λ α, of (mv_polynomial α ℤ), map := λ X Y f, ((rename f : mv_polynomial X ℤ →ₐ[ℤ] mv_polynomial Y ℤ) : (mv_polynomial X ℤ →+* mv_polynomial Y ℤ)), - -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it generates are too slow. + -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it + -- generates are too slow. map_id' := λ X, ring_hom.ext $ rename_id, map_comp' := λ X Y Z f g, ring_hom.ext $ λ p, (rename_rename f g p).symm } diff --git a/src/algebra/char_p.lean b/src/algebra/char_p.lean index 702b690c99d73..8320afb50877c 100644 --- a/src/algebra/char_p.lean +++ b/src/algebra/char_p.lean @@ -355,8 +355,8 @@ lemma char_p_of_ne_zero (hn : fintype.card R = n) (hR : ∀ i < n, (i : R) = 0 { rintro ⟨k, rfl⟩, rw [nat.cast_mul, H, zero_mul] } end } -lemma char_p_of_prime_pow_injective (p : ℕ) [hp : fact p.prime] (n : ℕ) (hn : fintype.card R = p ^ n) - (hR : ∀ i ≤ n, (p ^ i : R) = 0 → i = n) : +lemma char_p_of_prime_pow_injective (p : ℕ) [hp : fact p.prime] (n : ℕ) + (hn : fintype.card R = p ^ n) (hR : ∀ i ≤ n, (p ^ i : R) = 0 → i = n) : char_p R (p ^ n) := begin obtain ⟨c, hc⟩ := char_p.exists R, resetI, diff --git a/src/algebra/continued_fractions/computation/basic.lean b/src/algebra/continued_fractions/computation/basic.lean index 30fe9159a3887..641cf502bd5e3 100755 --- a/src/algebra/continued_fractions/computation/basic.lean +++ b/src/algebra/continued_fractions/computation/basic.lean @@ -14,10 +14,10 @@ import algebra.archimedean We formalise the standard computation of (regular) continued fractions for linear ordered floor fields. The algorithm is rather simple. Here is an outline of the procedure adapted from Wikipedia: -Take a value `v`. We call `⌊v⌋` the *integer part* of `v` and `v − ⌊v⌋` the *fractional part* of `v`. -A continued fraction representation of `v` can then be given by `[⌊v⌋; b₀, b₁, b₂,...]`, -where `[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v − ⌊v⌋)`. -This process stops when the fractional part hits 0. +Take a value `v`. We call `⌊v⌋` the *integer part* of `v` and `v − ⌊v⌋` the *fractional part* of +`v`. A continued fraction representation of `v` can then be given by `[⌊v⌋; b₀, b₁, b₂,...]`, where +`[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v − ⌊v⌋)`. This +process stops when the fractional part hits 0. In other words: to calculate a continued fraction representation of a number `v`, write down the integer part (i.e. the floor) of `v`. Subtract this integer part from `v`. If the difference is 0, @@ -113,7 +113,8 @@ Creates the stream of integer and fractional parts of a value `v` needed to obta fraction representation of `v` in `generalized_continued_fraction.of`. More precisely, given a value `v : K`, it recursively computes a stream of option `ℤ × K` pairs as follows: - `stream v 0 = some ⟨⌊v⌋, v - ⌊v⌋⟩` -- `stream v (n + 1) = some ⟨⌊frₙ⁻¹⌋, frₙ⁻¹ - ⌊frₙ⁻¹⌋⟩`, if `stream v n = some ⟨_, frₙ⟩` and `frₙ ≠ 0` +- `stream v (n + 1) = some ⟨⌊frₙ⁻¹⌋, frₙ⁻¹ - ⌊frₙ⁻¹⌋⟩`, + if `stream v n = some ⟨_, frₙ⟩` and `frₙ ≠ 0` - `stream v (n + 1) = none`, otherwise For example, let `(v : ℚ) := 3.4`. The process goes as follows: @@ -139,14 +140,14 @@ Uses `int_fract_pair.stream` to create a sequence with head (i.e. `seq1`) of int parts of a value `v`. The first value of `int_fract_pair.stream` is never `none`, so we can safely extract it and put the tail of the stream in the sequence part. -This is just an intermediate representation and users should not (need to) directly interact with it. -The setup of rewriting/simplification lemmas that make the definitions easy to use is done in +This is just an intermediate representation and users should not (need to) directly interact with +it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in `algebra.continued_fractions.computation.translations`. -/ protected def seq1 (v : K) : seq1 $ int_fract_pair K := ⟨ int_fract_pair.of v,--the head - seq.tail -- take the tail of `int_fract_pair.stream` since the first element is already in the head - -- create a sequence from `int_fract_pair.stream` + seq.tail -- take the tail of `int_fract_pair.stream` since the first element is already in the + -- head create a sequence from `int_fract_pair.stream` ⟨ int_fract_pair.stream v, -- the underlying stream @stream_is_seq _ _ _ v ⟩ ⟩ -- the proof that the stream is a sequence diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean index 0b32b820c9453..c27bc8418750f 100644 --- a/src/algebra/direct_limit.lean +++ b/src/algebra/direct_limit.lean @@ -40,7 +40,8 @@ namespace module variables [Π i, add_comm_group (G i)] [Π i, module R (G i)] -/-- A directed system is a functor from the category (directed poset) to the category of R-modules. -/ +/-- A directed system is a functor from the category (directed poset) to the category of +`R`-modules. -/ class directed_system (f : Π i j, i ≤ j → G i →ₗ[R] G j) : Prop := (map_self [] : ∀ i x h, f i i h x = x) (map_map [] : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x) @@ -143,8 +144,10 @@ begin simp [totalize_apply, hx k hk, le_trans (hx k hk) hij, directed_system.map_map f] end -lemma of.zero_exact_aux [nonempty ι] {x : direct_sum ι G} (H : submodule.quotient.mk x = (0 : direct_limit G f)) : - ∃ j, (∀ k ∈ x.support, k ≤ j) ∧ direct_sum.to_module R ι (G j) (λ i, totalize G f i j) x = (0 : G j) := +lemma of.zero_exact_aux [nonempty ι] {x : direct_sum ι G} + (H : submodule.quotient.mk x = (0 : direct_limit G f)) : + ∃ j, (∀ k ∈ x.support, k ≤ j) ∧ + direct_sum.to_module R ι (G j) (λ i, totalize G f i j) x = (0 : G j) := nonempty.elim (by apply_instance) $ assume ind : ι, span_induction ((quotient.mk_eq_zero _).1 H) (λ x ⟨i, j, hij, y, hxy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in @@ -234,9 +237,11 @@ linear_map.is_add_group_hom _ module.direct_limit.of_f @[simp] lemma of_zero (i) : of G f i 0 = 0 := is_add_group_hom.map_zero _ -@[simp] lemma of_add (i x y) : of G f i (x + y) = of G f i x + of G f i y := is_add_hom.map_add _ _ _ +@[simp] lemma of_add (i x y) : of G f i (x + y) = of G f i x + of G f i y := +is_add_hom.map_add _ _ _ @[simp] lemma of_neg (i x) : of G f i (-x) = -of G f i x := is_add_group_hom.map_neg _ _ -@[simp] lemma of_sub (i x y) : of G f i (x - y) = of G f i x - of G f i y := is_add_group_hom.map_sub _ _ _ +@[simp] lemma of_sub (i x y) : of G f i (x - y) = of G f i x - of G f i y := +is_add_group_hom.map_sub _ _ _ @[elab_as_eliminator] protected theorem induction_on [nonempty ι] {C : direct_limit G f → Prop} (z : direct_limit G f) @@ -268,9 +273,11 @@ linear_map.is_add_group_hom _ module.direct_limit.lift_of _ _ _ @[simp] lemma lift_zero : lift G f P g Hg 0 = 0 := is_add_group_hom.map_zero _ -@[simp] lemma lift_add (x y) : lift G f P g Hg (x + y) = lift G f P g Hg x + lift G f P g Hg y := is_add_hom.map_add _ _ _ +@[simp] lemma lift_add (x y) : lift G f P g Hg (x + y) = lift G f P g Hg x + lift G f P g Hg y := +is_add_hom.map_add _ _ _ @[simp] lemma lift_neg (x) : lift G f P g Hg (-x) = -lift G f P g Hg x := is_add_group_hom.map_neg _ _ -@[simp] lemma lift_sub (x y) : lift G f P g Hg (x - y) = lift G f P g Hg x - lift G f P g Hg y := is_add_group_hom.map_sub _ _ _ +@[simp] lemma lift_sub (x y) : lift G f P g Hg (x - y) = lift G f P g Hg x - lift G f P g Hg y := +is_add_group_hom.map_sub _ _ _ lemma lift_unique [nonempty ι] (F : direct_limit G f → P) [is_add_group_hom F] (x) : F x = @lift _ _ _ G _ f _ P _ (λ i x, F $ of G f i x) (λ i, is_add_group_hom.comp _ _) @@ -326,7 +333,8 @@ ideal.quotient.eq.2 $ subset_span $ or.inl ⟨i, j, hij, x, rfl⟩ @[simp] lemma of_neg (i x) : of G f i (-x) = -of G f i x := is_ring_hom.map_neg _ @[simp] lemma of_sub (i x y) : of G f i (x - y) = of G f i x - of G f i y := is_ring_hom.map_sub _ @[simp] lemma of_mul (i x y) : of G f i (x * y) = of G f i x * of G f i y := is_ring_hom.map_mul _ -@[simp] lemma of_pow (i x) (n : ℕ) : of G f i (x ^ n) = of G f i x ^ n := is_monoid_hom.map_pow _ _ _ +@[simp] lemma of_pow (i x) (n : ℕ) : of G f i (x ^ n) = of G f i x ^ n := +is_monoid_hom.map_pow _ _ _ /-- Every element of the direct limit corresponds to some element in some component of the directed system. -/ @@ -361,8 +369,8 @@ polynomial.induction_on q end -@[elab_as_eliminator] theorem induction_on [nonempty ι] {C : direct_limit G f → Prop} (z : direct_limit G f) - (ih : ∀ i x, C (of G f i x)) : C z := +@[elab_as_eliminator] theorem induction_on [nonempty ι] {C : direct_limit G f → Prop} + (z : direct_limit G f) (ih : ∀ i x, C (of G f i x)) : C z := let ⟨i, x, hx⟩ := exists_of z in hx ▸ ih i x section of_zero_exact @@ -399,7 +407,8 @@ begin end variables {G f} -lemma of.zero_exact_aux [nonempty ι] {x : free_comm_ring Σ i, G i} (H : ideal.quotient.mk _ x = (0 : direct_limit G f)) : +lemma of.zero_exact_aux [nonempty ι] {x : free_comm_ring Σ i, G i} + (H : ideal.quotient.mk _ x = (0 : direct_limit G f)) : ∃ j s, ∃ H : (∀ k : Σ i, G i, k ∈ s → k.1 ≤ j), is_supported x s ∧ lift (λ ix : s, f ix.1.1 j (H ix ix.2) ix.1.2) (restriction s x) = (0 : G j) := begin @@ -414,8 +423,8 @@ begin exacts [or.inr rfl, or.inl rfl] } }, { refine ⟨i, {⟨i, 1⟩}, _, is_supported_sub (is_supported_of.2 rfl) is_supported_one, _⟩, { rintros k (rfl|h), refl }, - { rw [(restriction _).map_sub, (free_comm_ring.lift _).map_sub, - restriction_of, dif_pos, (restriction _).map_one, lift_of, (free_comm_ring.lift _).map_one], + { rw [(restriction _).map_sub, (free_comm_ring.lift _).map_sub, restriction_of, dif_pos, + (restriction _).map_one, lift_of, (free_comm_ring.lift _).map_one], dsimp only, rw [is_ring_hom.map_one (f i i _), sub_self], { apply_assumption }, { exact set.mem_singleton _ } } }, @@ -462,8 +471,10 @@ begin rcases (s.image sigma.fst).exists_le with ⟨i, hi⟩, rcases directed_order.directed i j with ⟨k, hik, hjk⟩, have : ∀ z : Σ i, G i, z ∈ ↑s ∪ t → z.1 ≤ k, - { rintros z (hz | hz), exact le_trans (hi z.1 $ finset.mem_image.2 ⟨z, hz, rfl⟩) hik, exact le_trans (hj z hz) hjk }, - refine ⟨k, ↑s ∪ t, this, is_supported_mul (is_supported_upwards hxs $ set.subset_union_left ↑s t) + { rintros z (hz | hz), + exacts [(hi z.1 $ finset.mem_image.2 ⟨z, hz, rfl⟩).trans hik, (hj z hz).trans hjk] }, + refine ⟨k, ↑s ∪ t, this, is_supported_mul + (is_supported_upwards hxs $ set.subset_union_left ↑s t) (is_supported_upwards hyt $ set.subset_union_right ↑s t), _⟩, rw [(restriction _).map_mul, (free_comm_ring.lift _).map_mul, ← of.zero_exact_aux2 G f hyt hj this hjk (set.subset_union_right ↑s t), diff --git a/src/algebra/gcd_monoid.lean b/src/algebra/gcd_monoid.lean index ddf6a1996aef6..a45c187e8c665 100644 --- a/src/algebra/gcd_monoid.lean +++ b/src/algebra/gcd_monoid.lean @@ -63,7 +63,8 @@ set_option old_structure_cmd true -/-- Normalization monoid: multiplying with `norm_unit` gives a normal form for associated elements. -/ +/-- Normalization monoid: multiplying with `norm_unit` gives a normal form for associated +elements. -/ @[protect_proj] class normalization_monoid (α : Type*) [nontrivial α] [comm_cancel_monoid_with_zero α] := (norm_unit : α → units α) @@ -108,7 +109,8 @@ associates.mk_eq_mk_iff_associated.2 normalize_associated lemma normalize_coe_units (u : units α) : normalize (u : α) = 1 := by simp lemma normalize_eq_zero {x : α} : normalize x = 0 ↔ x = 0 := -⟨λ hx, (associated_zero_iff_eq_zero x).1 $ hx ▸ associated_normalize, by rintro rfl; exact normalize_zero⟩ +⟨λ hx, (associated_zero_iff_eq_zero x).1 $ hx ▸ associated_normalize, + by rintro rfl; exact normalize_zero⟩ lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x := ⟨λ hx, is_unit_iff_exists_inv.2 ⟨_, hx⟩, λ ⟨u, hu⟩, hu ▸ normalize_coe_units u⟩ @@ -186,10 +188,12 @@ quotient.induction_on₂ a b $ assume a b, by simp only [associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize.map_mul] lemma dvd_out_iff (a : α) (b : associates α) : a ∣ b.out ↔ associates.mk a ≤ b := -quotient.induction_on b $ by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff] +quotient.induction_on b $ + by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff] lemma out_dvd_iff (a : α) (b : associates α) : b.out ∣ a ↔ b ≤ associates.mk a := -quotient.induction_on b $ by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff] +quotient.induction_on b $ + by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff] @[simp] lemma out_top : (⊤ : associates α).out = 0 := normalize_zero @@ -246,7 +250,8 @@ theorem gcd_assoc (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k) := dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n)) - (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k))) + (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n)) + (gcd_dvd_right (gcd m n) k))) (dvd_gcd (dvd_gcd (gcd_dvd_left m (gcd n k)) (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k))) (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k))) @@ -283,7 +288,8 @@ dvd_gcd (dvd.trans (gcd_dvd_left _ _) hab) (dvd.trans (gcd_dvd_right _ _) hcd) gcd_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_refl a)) @[simp] theorem gcd_mul_left (a b c : α) : gcd (a * b) (a * c) = normalize a * gcd b c := -classical.by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero]) $ assume ha : a ≠ 0, +classical.by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero]) $ +assume ha : a ≠ 0, suffices gcd (a * b) (a * c) = normalize (a * gcd b c), by simpa only [normalize.map_mul, normalize_gcd], let ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c) in @@ -301,7 +307,8 @@ by simp only [mul_comm, gcd_mul_left] theorem gcd_eq_left_iff (a b : α) (h : normalize a = a) : gcd a b = a ↔ a ∣ b := iff.intro (assume eq, eq ▸ gcd_dvd_right _ _) $ - assume hab, dvd_antisymm_of_normalize_eq (normalize_gcd _ _) h (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) hab) + assume hab, dvd_antisymm_of_normalize_eq (normalize_gcd _ _) h (gcd_dvd_left _ _) + (dvd_gcd (dvd_refl a) hab) theorem gcd_eq_right_iff (a b : α) (h : normalize b = b) : gcd a b = b ↔ b ∣ a := by simpa only [gcd_comm a b] using gcd_eq_left_iff b a h @@ -520,7 +527,8 @@ iff.intro by rw [lcm_units_coe_left, normalize_coe_units]) @[simp] theorem lcm_mul_left (a b c : α) : lcm (a * b) (a * c) = normalize a * lcm b c := -classical.by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero]) $ assume ha : a ≠ 0, +classical.by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero]) $ +assume ha : a ≠ 0, suffices lcm (a * b) (a * c) = normalize (a * lcm b c), by simpa only [normalize.map_mul, normalize_lcm], have a ∣ lcm (a * b) (a * c), from dvd.trans (dvd_mul_right _ _) (dvd_lcm_left _ _), @@ -536,7 +544,8 @@ by simp only [mul_comm, lcm_mul_left] theorem lcm_eq_left_iff (a b : α) (h : normalize a = a) : lcm a b = a ↔ b ∣ a := iff.intro (assume eq, eq ▸ dvd_lcm_right _ _) $ - assume hab, dvd_antisymm_of_normalize_eq (normalize_lcm _ _) h (lcm_dvd (dvd_refl a) hab) (dvd_lcm_left _ _) + assume hab, dvd_antisymm_of_normalize_eq (normalize_lcm _ _) h (lcm_dvd (dvd_refl a) hab) + (dvd_lcm_left _ _) theorem lcm_eq_right_iff (a b : α) (h : normalize b = b) : lcm a b = b ↔ a ∣ b := by simpa only [lcm_comm b a] using lcm_eq_left_iff b a h diff --git a/src/algebra/geom_sum.lean b/src/algebra/geom_sum.lean index d710822abd216..b34d41e00e7fa 100644 --- a/src/algebra/geom_sum.lean +++ b/src/algebra/geom_sum.lean @@ -31,7 +31,8 @@ theorem geom_series_def [semiring α] (x : α) (n : ℕ) : geom_series x 1 = 1 := by { rw [geom_series_def, sum_range_one, pow_zero] } -@[simp] lemma op_geom_series [ring α] (x : α) (n : ℕ) : op (geom_series x n) = geom_series (op x) n := +@[simp] lemma op_geom_series [ring α] (x : α) (n : ℕ) : + op (geom_series x n) = geom_series (op x) n := by simp [geom_series_def] /-- Sum of the finite geometric series $\sum_{i=0}^{n-1} x^i y^{n-1-i}$. -/ @@ -179,7 +180,8 @@ have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x := begin rw [geom_sum h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃, ← mul_assoc, ← mul_assoc, mul_inv_cancel h₃], - simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄, sub_eq_add_neg, add_comm, add_left_comm], + simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄, sub_eq_add_neg, add_comm, + add_left_comm], end variables {β : Type*} diff --git a/src/algebra/monoid_algebra.lean b/src/algebra/monoid_algebra.lean index 34d9ebbac6aa0..013f48f6a3227 100644 --- a/src/algebra/monoid_algebra.lean +++ b/src/algebra/monoid_algebra.lean @@ -30,9 +30,9 @@ Unfortunately because additive and multiplicative structures both appear in both it doesn't appear to be possible to make much use of `to_additive`, and we just settle for saying everything twice. -Similarly, I attempted to just define `add_monoid_algebra k G := monoid_algebra k (multiplicative G)`, -but the definitional equality `multiplicative G = G` leaks through everywhere, and -seems impossible to use. +Similarly, I attempted to just define +`add_monoid_algebra k G := monoid_algebra k (multiplicative G)`, but the definitional equality +`multiplicative G = G` leaks through everywhere, and seems impossible to use. -/ noncomputable theory @@ -127,7 +127,8 @@ lemma lift_nc_mul (f : k →+* R) (g : G →* R) lift_nc (f : k →+ R) g (a * b) = lift_nc (f : k →+ R) g a * lift_nc (f : k →+ R) g b := begin conv_rhs { rw [← sum_single a, ← sum_single b] }, - simp_rw [mul_def, (lift_nc _ g).map_finsupp_sum, lift_nc_single, finsupp.sum_mul, finsupp.mul_sum], + simp_rw [mul_def, (lift_nc _ g).map_finsupp_sum, lift_nc_single, finsupp.sum_mul, + finsupp.mul_sum], refine finset.sum_congr rfl (λ y hy, finset.sum_congr rfl (λ x hx, _)), simp [mul_assoc, (h_comm hy).left_comm] end @@ -163,10 +164,12 @@ instance [ring k] [monoid G] : ring (monoid_algebra k G) := instance [comm_ring k] [comm_monoid G] : comm_ring (monoid_algebra k G) := { mul_comm := mul_comm, .. monoid_algebra.ring} -instance {R : Type*} [semiring R] [semiring k] [semimodule R k] : has_scalar R (monoid_algebra k G) := +instance {R : Type*} [semiring R] [semiring k] [semimodule R k] : + has_scalar R (monoid_algebra k G) := finsupp.has_scalar -instance {R : Type*} [semiring R] [semiring k] [semimodule R k] : semimodule R (monoid_algebra k G) := +instance {R : Type*} [semiring R] [semiring k] [semimodule R k] : + semimodule R (monoid_algebra k G) := finsupp.semimodule G k instance [group G] [semiring k] : distrib_mul_action G (monoid_algebra k G) := @@ -311,7 +314,8 @@ In particular this provides the instance `algebra k (monoid_algebra k G)`. instance {A : Type*} [comm_semiring k] [semiring A] [algebra k A] [monoid G] : algebra k (monoid_algebra A G) := { smul_def' := λ r a, by { ext, simp [single_one_mul_apply, algebra.smul_def''], }, - commutes' := λ r f, by { ext, simp [single_one_mul_apply, mul_single_one_apply, algebra.commutes], }, + commutes' := λ r f, by { ext, simp [single_one_mul_apply, mul_single_one_apply, + algebra.commutes], }, ..single_one_ring_hom.comp (algebra_map k A) } /-- `finsupp.single 1` as a `alg_hom` -/