Structures · Algebra
NonUnitalRing
An associative but not-necessarily unital ring.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Shape
- One type argument · adds mul_assoc
Extends2
Extended by4
Forgetful instances
Provided automatically by
Concrete types that are instances28
- SeparationQuotient
- Filter.Germ
- BoundedContinuousFunction
- CStarMatrix
- TensorProduct
- WithConv
- Matrix
- HahnSeries
- LocallyConstant
- MeasureTheory.SimpleFunc
- FreeAbelianGroup
- MonoidAlgebra
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- SkewMonoidAlgebra
- ZeroAtInftyContinuousMap
- RingCon.Quotient
- CompactlySupportedContinuousMap
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- ContinuousMap
- Shrink
How is a type an instance?
Loading the hierarchy index…
Assumed by501
- quasispectrum
- cfcₙ
- CFC.sqrt
- cfcₙHom
- CFC.abs
- cfcₙ_apply
- cfcₙ_apply_of_not_predicate
- cfcₙ_congr
- cfcₙ_id
- cfcₙ_apply_of_not_map_zero
- quasispectrum.zero_mem
- QuasispectrumRestricts.left_inv
- Unitization.quasispectrum_eq_spectrum_inr'
- CFC.sqrt_nonneg
- cfcₙHom_continuous
- CFC.sqrt_mul_sqrt_self
- cfcₙ_id'
- cfcₙ_comp'
- QuasispectrumRestricts.nonUnitalStarAlgHom
- cfcₙHom_id
- CFC.posPart_sub_negPart
- cfcₙ_apply_of_not_continuousOn
- cfcₙ_mul
- cfcₙ_cases
- CStarModule.innerₛₗ
- NonUnitalSubring.centralizer
- dvd_sub
- CFC.negPart_def
- cfcₙ_nnreal_eq_real
- CFC.posPart_def
- CFC.sqrt_eq_iff
- CFC.sqrt_eq_nnrpow
- cfcₙ.congr_simp
- CFC.sqrt.congr_simp
- cfcₙL
- dvd_add_left
- QuasispectrumRestricts.image
- cfcₙ_zero
- cfcₙ_def
- cfcₙHomSuperset
- cfcₙ_nonneg
- CFC.nnrpow_one
- CStarAlgebra.nonneg_TFAE
- IsSelfAdjoint.quasispectrumRestricts
- CFC.abs.congr_simp
- CFC.nnrpow
- CFC.abs_mul_abs
- QuasispectrumRestricts.rightInvOn
- dvd_add_right
- CFC.negPart_nonneg
Ancestors57
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Bracket
- Distrib
- Dvd
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Mul
- MulZeroClass
- NSMul
- Neg
- NegZeroClass
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalSemiring
- Nonempty
- OfNat
- One
- SMul
- Semigroup
- SemigroupWithZero
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero