Skip to content

Commit c6be01e

Browse files
Ruben-VandeVeldeRuben-VandeVelde
committed
chore: split out map_dvd (#19565)
1 parent cee87aa commit c6be01e

File tree

7 files changed

+39
-20
lines changed

7 files changed

+39
-20
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,7 @@ import Mathlib.Algebra.DirectSum.LinearMap
202202
import Mathlib.Algebra.DirectSum.Module
203203
import Mathlib.Algebra.DirectSum.Ring
204204
import Mathlib.Algebra.Divisibility.Basic
205+
import Mathlib.Algebra.Divisibility.Hom
205206
import Mathlib.Algebra.Divisibility.Prod
206207
import Mathlib.Algebra.Divisibility.Units
207208
import Mathlib.Algebra.DualNumber

‎Mathlib/Algebra/Divisibility/Basic.lean‎

Lines changed: 0 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston,
55
Neil Strickland, Aaron Anderson
66
-/
77
import Mathlib.Algebra.Group.Basic
8-
import Mathlib.Algebra.Group.Hom.Defs
98
import Mathlib.Tactic.Common
109

1110
/-!
@@ -83,22 +82,6 @@ alias Dvd.dvd.mul_right := dvd_mul_of_dvd_left
8382
theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
8483
(dvd_mul_right a b).trans h
8584

86-
section map_dvd
87-
88-
variable {M N : Type*}
89-
90-
theorem map_dvd [Semigroup M] [Semigroup N] {F : Type*} [FunLike F M N] [MulHomClass F M N]
91-
(f : F) {a b} : a ∣ b → f a ∣ f b
92-
| ⟨c, h⟩ => ⟨f c, h.symm ▸ map_mul f a c⟩
93-
94-
theorem MulHom.map_dvd [Semigroup M] [Semigroup N] (f : M →ₙ* N) {a b} : a ∣ b → f a ∣ f b :=
95-
_root_.map_dvd f
96-
97-
theorem MonoidHom.map_dvd [Monoid M] [Monoid N] (f : M →* N) {a b} : a ∣ b → f a ∣ f b :=
98-
_root_.map_dvd f
99-
100-
end map_dvd
101-
10285
/-- An element `a` in a semigroup is primal if whenever `a` is a divisor of `b * c`, it can be
10386
factored as the product of a divisor of `b` and a divisor of `c`. -/
10487
def IsPrimal (a : α) : Prop := ∀ ⦃b c⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

‎Mathlib/Algebra/Divisibility/Hom.lean‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
/-
2+
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
5+
Neil Strickland, Aaron Anderson
6+
-/
7+
import Mathlib.Algebra.Divisibility.Basic
8+
import Mathlib.Algebra.Group.Hom.Defs
9+
10+
/-!
11+
# Mapping divisibility across multiplication-preserving homomorphisms
12+
13+
## Main definitions
14+
15+
* `map_dvd`
16+
17+
## Tags
18+
19+
divisibility, divides
20+
-/
21+
22+
attribute [local simp] mul_assoc mul_comm mul_left_comm
23+
24+
variable {M N : Type*}
25+
26+
theorem map_dvd [Semigroup M] [Semigroup N] {F : Type*} [FunLike F M N] [MulHomClass F M N]
27+
(f : F) {a b} : a ∣ b → f a ∣ f b
28+
| ⟨c, h⟩ => ⟨f c, h.symm ▸ map_mul f a c⟩
29+
30+
theorem MulHom.map_dvd [Semigroup M] [Semigroup N] (f : M →ₙ* N) {a b} : a ∣ b → f a ∣ f b :=
31+
_root_.map_dvd f
32+
33+
theorem MonoidHom.map_dvd [Monoid M] [Monoid N] (f : M →* N) {a b} : a ∣ b → f a ∣ f b :=
34+
_root_.map_dvd f

‎Mathlib/Algebra/Prime/Lemmas.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Jens Wagemaker
55
-/
6+
import Mathlib.Algebra.Divisibility.Hom
67
import Mathlib.Algebra.Group.Commute.Units
78
import Mathlib.Algebra.Group.Even
89
import Mathlib.Algebra.Group.Units.Equiv

‎Mathlib/Algebra/Ring/Divisibility/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
55
-/
6-
import Mathlib.Algebra.Divisibility.Basic
6+
import Mathlib.Algebra.Divisibility.Hom
77
import Mathlib.Algebra.Group.Equiv.Basic
88
import Mathlib.Algebra.Ring.Defs
99

‎Mathlib/Algebra/Ring/Hom/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2019 Amelia Livingston. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Amelia Livingston, Jireh Loreaux
55
-/
6-
import Mathlib.Algebra.Divisibility.Basic
6+
import Mathlib.Algebra.Divisibility.Hom
77
import Mathlib.Algebra.GroupWithZero.InjSurj
88
import Mathlib.Algebra.Ring.Hom.Defs
99
import Mathlib.Data.Set.Basic

‎Mathlib/Data/Nat/Cast/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Mathlib.Algebra.Divisibility.Basic
6+
import Mathlib.Algebra.Divisibility.Hom
77
import Mathlib.Algebra.Group.Even
88
import Mathlib.Algebra.Group.TypeTags.Hom
99
import Mathlib.Algebra.Ring.Hom.Defs

0 commit comments

Comments
 (0)