Theorems · Theorem
Function.Semiconj.comp_eq
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β}, Function.Semiconj f ga gb → f ∘ ga = gb ∘ fAlias of the forward direction of Function.semiconj_iff_comp_eq.
Definition of Function.Semiconj in terms of functional equality.
- Defined in
- Mathlib.Logic.Function.Conjugate
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.Semiconjstatement · cited by 82
- Function.semiconj_iff_comp_eqproof · cited by 2
Cited by11
Results whose statement or proof uses this declaration.
- Function.iterate_succ'proof · cited by 56
- Function.Semiconj.filter_mapproof · cited by 3
- Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprimeproof · cited by 2
- Function.Semiconj.preimage_dynEntourageproof · cited by 2
- MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_semiconjproof · cited by 2
- MeasureTheory.MeasurePreserving.of_semiconjproof · cited by 1
- Function.Semiconj.filter_comapproof · cited by 1
- Function.Commute.left_bijOn_fixedPoints_compproof · cited by 0
- MeasurableSpace.measurable_invariants_of_semiconjproof · cited by 0
- Function.Commute.right_bijOn_fixedPoints_compproof · cited by 0
- Function.Commute.invOn_fixedPoints_compproof · cited by 0