-
Notifications
You must be signed in to change notification settings - Fork 312
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: split Algebra.Semiconj and Algebra.Commute (#7098)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
- Loading branch information
Showing
19 changed files
with
418 additions
and
275 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,61 @@ | ||
/- | ||
Copyright (c) 2019 Neil Strickland. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Neil Strickland, Yury Kudryashov | ||
-/ | ||
import Mathlib.Algebra.Group.Commute.Defs | ||
import Mathlib.Algebra.Group.Semiconj.Basic | ||
|
||
#align_import algebra.group.commute from "leanprover-community/mathlib"@"05101c3df9d9cfe9430edc205860c79b6d660102" | ||
|
||
/-! | ||
# Additional lemmas about commuting pairs of elements in monoids | ||
-/ | ||
|
||
|
||
variable {G : Type*} | ||
|
||
namespace Commute | ||
|
||
section DivisionMonoid | ||
|
||
variable [DivisionMonoid G] {a b c d: G} | ||
|
||
@[to_additive] | ||
protected theorem inv_inv : Commute a b → Commute a⁻¹ b⁻¹ := | ||
SemiconjBy.inv_inv_symm | ||
#align commute.inv_inv Commute.inv_inv | ||
#align add_commute.neg_neg AddCommute.neg_neg | ||
|
||
@[to_additive (attr := simp)] | ||
theorem inv_inv_iff : Commute a⁻¹ b⁻¹ ↔ Commute a b := | ||
SemiconjBy.inv_inv_symm_iff | ||
#align commute.inv_inv_iff Commute.inv_inv_iff | ||
#align add_commute.neg_neg_iff AddCommute.neg_neg_iff | ||
|
||
@[to_additive] | ||
protected theorem div_mul_div_comm (hbd : Commute b d) (hbc : Commute b⁻¹ c) : | ||
a / b * (c / d) = a * c / (b * d) := by | ||
simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm] | ||
#align commute.div_mul_div_comm Commute.div_mul_div_comm | ||
#align add_commute.sub_add_sub_comm AddCommute.sub_add_sub_comm | ||
|
||
@[to_additive] | ||
protected theorem mul_div_mul_comm (hcd : Commute c d) (hbc : Commute b c⁻¹) : | ||
a * b / (c * d) = a / c * (b / d) := | ||
(hcd.div_mul_div_comm hbc.symm).symm | ||
#align commute.mul_div_mul_comm Commute.mul_div_mul_comm | ||
#align add_commute.add_sub_add_comm AddCommute.add_sub_add_comm | ||
|
||
@[to_additive] | ||
protected theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d) (hcd : Commute c⁻¹ d) : | ||
a / b / (c / d) = a / c / (b / d) := by | ||
simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq, | ||
hbc.inv_inv.mul_mul_mul_comm] | ||
#align commute.div_div_div_comm Commute.div_div_div_comm | ||
#align add_commute.sub_sub_sub_comm AddCommute.sub_sub_sub_comm | ||
|
||
end DivisionMonoid | ||
|
||
end Commute |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.