Mathlib Map

Theorems · Theorem · field theory

UniformSpace.Completion.hatInv_extends

∀ {K : Type u_1} [inst : Field K] [inst_1 : UniformSpace K] [IsTopologicalDivisionRing K] {x : K},
  x ≠ 0 → (↑x).hatInv = ↑x⁻¹
Defined in
Mathlib.Topology.Algebra.UniformField
Cited by
2 results in Mathlib
Foundations
Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldUniformSpaceIsTopologicalDivisionRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

UniformSpace.Completion.coe_inv · cited by 0Completion.coe_invUniformSpace.Completion.mul_hatInv_cancel · cited by 0Completion.mul_hatInv_can…Field · cited by 7404FieldUniformSpace · cited by 2040UniformSpaceContinuous.continuousAt · cited by 297Continuous.continuousAtUniformSpace.Completion · cited by 192UniformSpace.CompletionUniformSpace.Completion.coe' · cited by 144Completion.coe'ContinuousAt.comp · cited by 56ContinuousAt.compUniformSpace.Completion.isDenseInducing_coe · cited by 11Completion.isDenseInducin…UniformSpace.Completion.continuous_coe · cited by 8Completion.continuous_coeIsTopologicalDivisionRing · cited by 8IsTopologicalDivisionRingIsDenseInducing.extend_eq_at · cited by 6IsDenseInducing.extend_eq…ContinuousInv₀.continuousAt_inv₀ · cited by 5ContinuousInv₀.continuous…UniformSpace.Completion.hatInv · cited by 4Completion.hatInvCompletion.hatInv_extendsCITED BYCITES

Cites12

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

Cited by2

Results whose statement or proof uses this declaration.