No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
774theorem multiplicative (f : JAut) (x y : PosReal) :
775 f (posMul x y) = posMul (f x) (f y) :=
proof body
Term-mode proof.
776 f.2.1 x y
777
778/-- Cost preservation of a `J`-automorphism. -/
used by (40)
From the project-wide theorem graph. These declarations reference this one in their body.
-
comp
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
cost_algebra_unique_aczel
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
CostMorphism
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
CostMorphism
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
CostMorphism
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
eq_id_of_map_two_eq_two
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
equivZModTwo
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
H_at_one
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
J
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
J_defect_form
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
J_at_phi
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
PhiInt
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
PhiInt
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
PhiInt
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
PhiInt
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
phi_ring_certificate
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
CostAlgHomKappa
in IndisputableMonolith.Algebra.RecognitionCategory
decl_use
-
CostAlgPlusHom
in IndisputableMonolith.Algebra.RecognitionCategory
decl_use
-
initial_morphism_exists
in IndisputableMonolith.Algebra.RecognitionCategory
decl_use
-
powerMap_pos
in IndisputableMonolith.Algebra.RecognitionCategory
decl_use
-
p_neq_np_conditional
in IndisputableMonolith.Complexity.CircuitLowerBound
decl_use
-
H_from_phi
in IndisputableMonolith.Cost.CauchyAuxiliary
decl_use
-
H_PhiMultiplicative
in IndisputableMonolith.Cost.CauchyAuxiliary
decl_use
-
additiveQuadratic
in IndisputableMonolith.Cost.Ndim.Bridge
decl_use
-
dot_sq_le_sqNorm_mul
in IndisputableMonolith.Cost.Ndim.Bridge
decl_use
-
oncologyLatticeCert
in IndisputableMonolith.CrossDomain.OncologyLattice
decl_use
-
OncologyLatticeCert
in IndisputableMonolith.CrossDomain.OncologyLattice
decl_use
-
perTurn_ratio
in IndisputableMonolith.Flight.Geometry
decl_use
-
back
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
Normalization
in IndisputableMonolith.Foundation.CostAxioms
decl_use
… and 10 more
depends on (9)
Lean names referenced from this declaration's body.
-
JAut
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
posMul
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
PosReal
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use