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] - feat: port LinearAlgebra.Matrix.NonsingularInverse #3647

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: port LinearAlgebra.Matrix.NonsingularInverse #3647

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
ebd3c06
feat: port LinearAlgebra.Matrix.NonsingularInverse
Ruben-VandeVelde Apr 25, 2023
0f7fe02
Initial file copy from mathport
Ruben-VandeVelde Apr 25, 2023
3c50d41
automated fixes
Ruben-VandeVelde Apr 25, 2023
9f59d48
Initial fixes
Ruben-VandeVelde Apr 25, 2023
ef43d76
Fixes
Ruben-VandeVelde Apr 25, 2023
8dd775d
Fixes
Ruben-VandeVelde Apr 25, 2023
32c65b7
Automated
Ruben-VandeVelde Apr 25, 2023
97f465a
Tidy
Ruben-VandeVelde Apr 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1403,6 +1403,7 @@ import Mathlib.LinearAlgebra.Matrix.Determinant
import Mathlib.LinearAlgebra.Matrix.DotProduct
import Mathlib.LinearAlgebra.Matrix.MvPolynomial
import Mathlib.LinearAlgebra.Matrix.Nondegenerate
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.Orthogonal
import Mathlib.LinearAlgebra.Matrix.Polynomial
import Mathlib.LinearAlgebra.Matrix.Reindex
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Group/Units.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,9 +114,9 @@ attribute [instance] AddUnits.instCoeHeadAddUnits

/-- The inverse of a unit in a `Monoid`. -/
@[to_additive "The additive inverse of an additive unit in an `AddMonoid`."]
instance : Inv αˣ :=
instance instInv : Inv αˣ :=
⟨fun u => ⟨u.2, u.1, u.4, u.3⟩⟩
attribute [instance] AddUnits.instNegAddUnits
attribute [instance] AddUnits.instNeg

/- porting note: the result of these definitions is syntactically equal to `Units.val` and
`Units.inv` because of the way coercions work in Lean 4, so there is no need for these custom
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Algebra/Invertible.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,10 +161,11 @@ theorem invertible_unique {α : Type u} [Monoid α] (a b : α) [Invertible a] [I
rw [h, mul_invOf_self]
#align invertible_unique invertible_unique

instance [Monoid α] (a : α) : Subsingleton (Invertible a) :=
instance Invertible.subsingleton [Monoid α] (a : α) : Subsingleton (Invertible a) :=
⟨fun ⟨b, hba, hab⟩ ⟨c, _, hac⟩ => by
congr
exact left_inv_eq_right_inv hba hac⟩
#align invertible.subsingleton Invertible.subsingleton

/-- If `r` is invertible and `s = r`, then `s` is invertible. -/
def Invertible.copy [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs : s = r) :
Expand Down
Loading
Loading