Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: forward-port leanprover-community/mathlib#18958 #3920

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore: forward-port leanprover-community/mathlib#18958 #3920

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f66ae52
refactor: Redefine `a ≡ b [PMOD p]`
YaelDillies May 11, 2023
4cc2ea1
Update Mathlib/Algebra/Hom/Units.lean
eric-wieser May 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
7 changes: 6 additions & 1 deletion Mathlib/Algebra/Group/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro

! This file was ported from Lean 3 source module algebra.group.basic
! leanprover-community/mathlib commit 84771a9f5f0bd5e5d6218811556508ddf476dcbd
! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c

Check notice on line 7 in Mathlib/Algebra/Group/Basic.lean

View workflow job for this annotation

GitHub Actions / Add annotations

Synchronization 

See https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=84771a9f5f0bd5e5d6218811556508ddf476dcbd..a07d750983b94c530ab69a726862c2ab6802b38c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -755,6 +755,11 @@
#align mul_div_cancel'' mul_div_cancel''
#align add_sub_cancel add_sub_cancel

@[to_additive (attr := simp) sub_add_cancel'']
theorem div_mul_cancel''' (a b : G) : a / (b * a) = b⁻¹ := by rw [← inv_div, mul_div_cancel'']
#align div_mul_cancel''' div_mul_cancel'''
#align sub_add_cancel'' sub_add_cancel''

@[to_additive (attr := simp)]
theorem mul_div_mul_right_eq_div (a b c : G) : a * c / (b * c) = a / b := by
rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
Expand Down
9 changes: 8 additions & 1 deletion Mathlib/Algebra/GroupPower/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
Authors: Jeremy Avigad, Robert Y. Lewis

! This file was ported from Lean 3 source module algebra.group_power.lemmas
! leanprover-community/mathlib commit e655e4ea5c6d02854696f97494997ba4c31be802
! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c

Check notice on line 7 in Mathlib/Algebra/GroupPower/Lemmas.lean

View workflow job for this annotation

GitHub Actions / Add annotations

Synchronization 

See https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_power/lemmas?range=e655e4ea5c6d02854696f97494997ba4c31be802..a07d750983b94c530ab69a726862c2ab6802b38c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -579,6 +579,13 @@

end bit0_bit1

/-- Note this holds in marginally more generality than `Int.cast_mul` -/
theorem Int.cast_mul_eq_zsmul_cast [AddCommGroupWithOne α] : ∀ m n, ((m * n : ℤ) : α) = m • n :=
fun m =>
Int.inductionOn' m 0 (by simp) (fun k _ ih n => by simp [add_mul, add_zsmul, ih]) fun k _ ih n =>
by simp [sub_mul, sub_zsmul, ih, ← sub_eq_add_neg]
#align int.cast_mul_eq_zsmul_cast Int.cast_mul_eq_zsmul_cast

@[simp]
theorem zsmul_eq_mul [Ring R] (a : R) : ∀ n : ℤ, n • a = n * a
| (n : ℕ) => by rw [coe_nat_zsmul, nsmul_eq_mul, Int.cast_ofNat]
Expand Down
5 changes: 3 additions & 2 deletions Mathlib/Algebra/Hom/Units.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
Ported by: Winston Yin

! This file was ported from Lean 3 source module algebra.hom.units
! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c

Check notice on line 8 in Mathlib/Algebra/Hom/Units.lean

View workflow job for this annotation

GitHub Actions / Add annotations

Synchronization 

See https://leanprover-community.github.io/mathlib-port-status/file/algebra/hom/units?range=dc6c365e751e34d100e80fe6e314c3c3e0fd2988..a07d750983b94c530ab69a726862c2ab6802b38c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -437,7 +437,8 @@
#align is_unit.div_eq_one_iff_eq IsUnit.div_eq_one_iff_eq
#align is_add_unit.sub_eq_zero_iff_eq IsAddUnit.sub_eq_zero_iff_eq

@[to_additive]
/-- The `group` version of this lemma is `div_mul_cancel'''` -/
@[to_additive "The `add_group` version of this lemma is `sub_add_cancel''`"]
eric-wieser marked this conversation as resolved.
Show resolved Hide resolved
protected theorem div_mul_left (h : IsUnit b) : b / (a * b) = 1 / a := by
rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div]
#align is_unit.div_mul_left IsUnit.div_mul_left
Expand Down