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)
764def JAut : Type :=
proof body
Definition body.
765 { f : PosReal → PosReal //
766 (∀ x y : PosReal, f (posMul x y) = posMul (f x) (f y)) ∧
767 (∀ x : PosReal, J (f x).1 = J x.1) }
768
769namespace JAut
770
771instance : CoeFun JAut (fun _ => PosReal → PosReal) := ⟨fun f => f.1⟩
772
773/-- Multiplicativity of a `J`-automorphism. -/
used by (17)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (7)
Lean names referenced from this declaration's body.
-
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