Theorems · Theorem · functional analysis
Unitization.isQuasiregular_inr_iff
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A]
[inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (a : A), IsQuasiregular ↑a ↔ IsQuasiregular a- Cited by
- 2 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- CommSemiringstatement and proof · cited by 10,911
- IsScalarTowerstatement and proof · cited by 3,896
- add_zeroproof · cited by 2,707
- SMulCommClassstatement and proof · cited by 1,927
- MulZeroClass.zero_mulproof · cited by 1,625
- NonUnitalRingstatement and proof · cited by 422
- Unitizationstatement and proof · cited by 220
- Unitization.inrstatement and proof · cited by 109
- Unitization.toProdproof · cited by 76
- IsQuasiregularstatement and proof · cited by 18
Cited by2
Results whose statement or proof uses this declaration.
- Unitization.quasispectrum_eq_spectrum_inr'proof · cited by 12
- Unitization.quasispectrum_eq_spectrum_inrproof · cited by 4