[Merged by Bors] - chore: fix most phantom #aligns #1794
Conversation
rwbarton
commented
Jan 23, 2023
rwbarton
commented
| @@ -239,11 +239,13 @@ theorem coe_mul {α : Type u} [Mul α] {a b : α} : ((a * b : α) : WithZero α) | |||
| -- prove it because we've just proved we're in MulZeroClass. | |||
| theorem zero_mul {α : Type u} [Mul α] (a : WithZero α) : 0 * a = 0 := | |||
| rfl | |||
| #align with_zero.zero_mul WithZero.zero_mul | |||
| -- Porting note: This lemma and the next one | |||
There was a problem hiding this comment.
Have you looked into why that is? Otherwise maybe leave it for now?
There was a problem hiding this comment.
Well with_zero.zero_mul definitely doesn't exist. So it doesn't make a lot of sense for it to have an #align, right? regardless of what else is going on?
But we could just leave an erroneous align, as well (it's not like there will be none, after this PR).
| @@ -135,13 +135,13 @@ theorem Commute.mul_pow {a b : M} (h : Commute a b) (n : ℕ) : (a * b) ^ n = a | |||
| · rw [pow_zero, pow_zero, pow_zero, one_mul] | |||
| · simp only [pow_succ, ih, ← mul_assoc, (h.pow_left n).right_comm] | |||
| #align commute.mul_pow Commute.mul_pow | |||
| #align add_commute.add_smul AddCommute.add_smul | |||
| #align add_commute.add_nsmul AddCommute.add_smul | |||
There was a problem hiding this comment.
It turns out these are wrong on the mathlib4 side. Should we fix the names here as well?
There was a problem hiding this comment.
There is a separate PR #1502 for that (which will unfortunately have a lot of merge conflicts with this one...)
| @@ -33,7 +33,7 @@ protected def mulLeft₀ (a : G) (ha : a ≠ 0) : Perm G := | |||
|
|
|||
| theorem mulLeft_bijective₀ (a : G) (ha : a ≠ 0) : Function.Bijective ((· * ·) a : G → G) := | |||
| (Equiv.mulLeft₀ a ha).bijective | |||
| #align equiv.mul_left_bijective₀ Equiv.mulLeft_bijective₀ | |||
There was a problem hiding this comment.
Missing _root_.? I'm also not sure this is translated correctly.
There was a problem hiding this comment.
I would sort of prefer to only change #aligns in this PR.
We can make a note of the name changes for another PR.
| @@ -35,7 +35,7 @@ namespace Pi | |||
| theorem IsSMulRegular.pi {α : Type _} [∀ i, SMul α <| f i] {k : α} | |||
| (hk : ∀ i, IsSMulRegular (f i) k) : IsSMulRegular (∀ i, f i) k := fun _ _ h => | |||
| funext fun i => hk i (congr_fun h i : _) | |||
| #align pi.is_smul_regular.pi Pi.IsSMulRegular.pi | |||
| @@ -40,22 +40,22 @@ theorem coe_add (x y : { x : M // 0 < x }) : ↑(x + y) = (x + y : M) := | |||
|
|
|||
| instance addSemigroup : AddSemigroup { x : M // 0 < x } := | |||
| Subtype.coe_injective.addSemigroup _ coe_add | |||
| #align subtype.add_semigroup Positive.addSemigroup | |||
| #align positive.subtype.add_semigroup Positive.addSemigroup | |||
There was a problem hiding this comment.
| @@ -816,13 +816,13 @@ theorem exists_lt (f : CauSeq α abs) : ∃ a : α, const a < f := | |||
| theorem rat_sup_continuous_lemma {ε : α} {a₁ a₂ b₁ b₂ : α} : | |||
| abs (a₁ - b₁) < ε → abs (a₂ - b₂) < ε → abs (a₁ ⊔ a₂ - b₁ ⊔ b₂) < ε := fun h₁ h₂ => | |||
| (abs_max_sub_max_le_max _ _ _ _).trans_lt (max_lt h₁ h₂) | |||
| #align cau_seq.rat_sup_continuous_lemma CauSeq.rat_sup_continuous_lemma | |||
| #align rat_sup_continuous_lemma CauSeq.rat_sup_continuous_lemma | |||
There was a problem hiding this comment.
|
|
||
| #align equiv.remove_none_aux Equiv.removeNone_aux | ||
| -- Porting note: private | ||
| -- #align equiv.remove_none_aux Equiv.removeNone_aux |
There was a problem hiding this comment.
Should we make it private as well
There was a problem hiding this comment.
Probably but maybe in a separate PR?
|
Thanks 🎉 bors merge |
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
* [ ] depends on: #1794 Implements a linter for lean 3 declarations containing capital letters (as [suggested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/non-aligned.20definitions/near/323102645)). Co-authored-by: Mario Carneiro <di.gama@gmail.com>
* [ ] depends on: #1794 Implements a linter for lean 3 declarations containing capital letters (as [suggested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/non-aligned.20definitions/near/323102645)). Co-authored-by: Mario Carneiro <di.gama@gmail.com>
