Structures · Algebra
FaithfulSMul
Typeclass for faithful actions.
- Defined in
- Mathlib.Algebra.Group.Action.Faithful
- Shape
- 2 explicit arguments · adds eq_of_smul_eq_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances30
- Int
- Nat
- ContinuousLinearMap
- Polynomial
- WithVal
- DomMulAct
- Units
- Module.End
- AlgEquiv
- Algebra.Presentation.Core
- AddMonoid.End
- LinearEquiv
- Equiv.Perm
- MvPolynomial
- RegularWreathProduct
- RelIso
- RelEmbedding
- RingAut
- MulAut
- Matrix.ProjGenLinGroup
- HNNExtension
- Monoid.PushoutI
- RelHom
- Function.End
- Matrix.ProjectiveSpecialLinearGroup
- Subtype
- MulOpposite
- HasQuotient.Quotient
- WithAbs
- RingHom
How is a type an instance?
Loading the hierarchy index…
Assumed by423
- FaithfulSMul.algebraMap_injective
- FractionRing.liftAlgebra
- RootPairing.posRootForm
- RootPairing.RootPositiveForm.posForm
- FaithfulSMul.eq_of_smul_eq_smul
- AlgebraicIndependent.matroid
- RatFunc.liftAlgebra
- RootPairing.RootFormIn
- RootPairing.PolarizationIn
- LinearIndependent.restrict_scalars'
- RootPairing.coroot'In
- RootPairing.pairingIn_reflectionPerm_self_left
- RootPairing.RootPositiveForm.toInvariantForm
- IsGaloisGroup.mulEquivAlgEquiv
- IsDomain.of_faithfulSMul
- Submodule.unitsToPic
- IsGaloisGroup.ringEquivFixedPoints
- RootPairing.RootPositiveForm.rootLength
- RootPairing.pairingIn_same
- FaithfulSMul.algebraMap_eq_zero_iff
- RootPairing.RootPositiveForm.algebraMap_posForm
- Ideal.map_ne_bot_of_ne_bot
- RootPairing.pairingIn_reflectionPerm_self_right
- FaithfulSMul.trans
- Module.IsTorsionFree.trans_faithfulSMul
- IsGaloisGroup.ringEquivFixedPoints_apply_coe
- IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply
- RootPairing.algebraMap_rootFormIn
- exists_isTranscendenceBasis
- IsGaloisGroup.mulEquivCongr
- RootPairing.Base.cartanMatrixIn_apply_same
- IsGaloisGroup.restrictHom
- RootPairing.pairingIn_eq_zero_iff
- Ideal.ne_bot_of_liesOver_of_ne_bot
- IsAlgClosed.exists_aeval_eq_zero
- RootPairing.RootPositiveForm.zero_lt_posForm_apply_root
- RootPairing.posRootForm_eq
- Module.finrank_top_le_finrank_of_isScalarTower
- AlgebraicIndependent.matroid_cRank_eq
- RootPairing.PolarizationIn_apply
- IsGaloisGroup.quotientMulEquiv
- Submodule.range_unitsToPic
- RootPairing.PolarizationIn_eq
- IsGaloisGroup.mulEquivAlgEquiv_apply_apply
- RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul
- FixedPoints.finrank_eq_card
- RootPairing.algebraMap_coroot'In_apply
- IsBaseChange.lift_rank_eq
- Ideal.exists_maximal_ideal_liesOver_of_isIntegral
- IsGaloisGroup.mulEquivCongr_apply_smul
Ancestors0
No ancestors.