Structures · Algebra
Invertible
Invertible a gives a two-sided multiplicative inverse of a.
- Defined in
- Mathlib.Algebra.Group.Invertible.Defs
- Shape
- One type argument · adds invOf, invOf_mul_self, mul_invOf_self
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- Matrix
- SymAlg
- ArithmeticFunction
- Module.End
- MvPolynomial
- LaurentPolynomial
How is a type an instance?
Loading the hierarchy index…
Assumed by560
- Invertible.invOf
- midpoint
- invOf_eq_inv
- QuadraticMap.associated
- QuadraticForm.tmul
- QuadraticMap.associatedHom
- mul_invOf_self
- isUnit_of_invertible
- xInTermsOfW
- invOf_mul_self
- Invertible.congr
- QuadraticForm.baseChange
- skewAdjointPart
- midpoint_comm
- QuadraticForm.toMatrix'
- Ring.inverse_invertible
- Matrix.invOf_eq_nonsing_inv
- CliffordAlgebra.toBaseChange
- invOf_eq_right_inv
- Invertible.ne_zero
- selfAdjointPart
- PowerSeries.substInv
- QuadraticForm.toMatrix
- midpoint_self
- skewAdjointPart_apply_coe
- midpoint_eq_iff
- xInTermsOfW_eq
- QuadraticMap.associated_eq_self_apply
- invOf_units
- CliffordAlgebra.ofBaseChange
- Matrix.inv_mul_of_invertible
- dist_left_midpoint
- unitOfInvertible
- left_vsub_midpoint
- xInTermsOfW_zero
- Matrix.isUnit_det_of_invertible
- Matrix.inv_inv_of_invertible
- invOf_two_smul_add_invOf_two_smul
- QuadraticMap.associated_comp
- midpoint_eq_smul_add
- QuadraticForm.associated_tmul
- Invertible.map
- midpoint_vsub_left
- WeierstrassCurve.toCharNeTwoNF
- QuadraticForm.tensorAssoc
- QuadraticForm.discr'
- QuadraticForm.tensorRId
- selfAdjointPart_apply_coe
- AffineEquiv.pointReflection_midpoint_left
- right_vsub_midpoint
Ancestors0
No ancestors.