Theorems · Theorem · group theory
MulEquiv.irreducible_iff
∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] {x : M} [inst_2 : EquivLike F M N]
[MulEquivClass F M N] (f : F), Irreducible (f x) ↔ Irreducible x- Defined in
- Mathlib.Algebra.Group.Irreducible.Lemmas
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- IsUnitproof · cited by 1,602
- Irreduciblestatement · cited by 496
- Function.Surjective.forallproof · cited by 214
- EquivLikestatement and proof · cited by 165
- MulEquivClassstatement and proof · cited by 30
- EquivLike.surjectiveproof · cited by 24
Cited by3
Results whose statement or proof uses this declaration.
- RatFunc.irreducible_minpolyX'proof · cited by 1
- Irreducible.mapproof · cited by 1
- minpoly.map_eq_of_equiv_equivproof · cited by 1