Theorems · Definition · general topology

LocallyConstant.congrRightRingEquiv

{X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        [inst_1 : Semiring Y] → [inst_2 : Semiring Z] → Y ≃+* Z → LocallyConstant X Y ≃+* LocallyConstant X Z

LocallyConstant.congrRight as a RingEquiv.

Defined in: Mathlib.Topology.LocallyConstant.Algebra
Cited by: 2 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace Semiring Semiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Semiringstatement and proof · cited by 13,802
Equivproof · cited by 8,337
MonoidHomproof · cited by 3,629
AddMonoidHomproof · cited by 3,230
RingEquivstatement and proof · cited by 1,147
LocallyConstantstatement and proof · cited by 227
EquivLike.toEquivproof · cited by 125
RingEquiv.toMonoidHomproof · cited by 13
LocallyConstant.congrRightproof · cited by 2
RingEquiv.toAddMonoidHomproof · cited by 1
LocallyConstant.mapAddMonoidHomproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

LocallyConstant.congrRightRingEquiv_apply_applystatement and proof · cited by 0
LocallyConstant.congrRightRingEquiv_symm_apply_applystatement and proof · cited by 0