def definition def or abbrev

`inv`

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

formal statement (Lean)

  44@[simp] def inv (r : Ribbon) : Ribbon := { r with dir := ! r.dir, bit := - r.bit }

Definition body.

  45
  46/-- Cancellation predicate for adjacent syllables (tick consistency abstracted). -/

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

toComplex_inv in IndisputableMonolith.Foundation.ComplexFromLogic 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 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.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Ribbon in IndisputableMonolith.Masses.Ribbons decl_use
Ribbon in IndisputableMonolith.Masses.Ribbons.Word decl_use
dir in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
inv in IndisputableMonolith.RecogSpec.Core decl_use