[Merged by Bors] - chore: fix most phantom #aligns#1794
[Merged by Bors] - chore: fix most phantom #aligns#1794
Conversation
rwbarton
commented
Jan 23, 2023
| 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).
| · 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...)
|
|
||
| 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.
| 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 |
| 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.
| 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:
|
* [ ] 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>