lemma proved term proof

`inv`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  89lemma inv (hx : PhiClosed φ x) : PhiClosed φ x⁻¹ :=

Term-mode proof.

  90  (phiSubfield φ).inv_mem hx
  91

From the project-wide theorem graph. These declarations reference this one in their body.

toComplex_inv in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
inv in IndisputableMonolith.Masses.Ribbons decl_use
rm2Closed_of_coerciveL2Bound in IndisputableMonolith.NavierStokes.RM2U.RM2Closure decl_use
zetaReciprocal_differentiableAt in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
zetaReciprocal_meromorphicAt in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
compAutomorphism_inv_left_eq_id in IndisputableMonolith.RecogGeom.Symmetry decl_use
compAutomorphism_inv_left_toFun in IndisputableMonolith.RecogGeom.Symmetry decl_use
compAutomorphism_inv_right_eq_id in IndisputableMonolith.RecogGeom.Symmetry decl_use
compAutomorphism_inv_right_toFun in IndisputableMonolith.RecogGeom.Symmetry decl_use
gaugeEquivalent_symm in IndisputableMonolith.RecogGeom.Symmetry decl_use
RecognitionAutomorphism in IndisputableMonolith.RecogGeom.Symmetry decl_use
symmetry_status in IndisputableMonolith.RecogGeom.Symmetry decl_use
half in IndisputableMonolith.RecogSpec.Core decl_use
inv_pow_self in IndisputableMonolith.RecogSpec.Core decl_use
inv_self in IndisputableMonolith.RecogSpec.Core decl_use
partialDeriv_v2_radialInv in IndisputableMonolith.Relativity.Calculus.Derivatives decl_use
partialDeriv_v2_radialInv_proved in IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs decl_use
lnal_manifest_json in IndisputableMonolith.URCAdapters.LNALReports decl_use

Lean names referenced from this declaration's body.