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)
732abbrev PosReal := {x : ℝ // 0 < x}
proof body
Definition body.
733
734/-- Multiplication on positive reals. -/
used by (16)
From the project-wide theorem graph. These declarations reference this one in their body.
-
comp_apply
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
continuous_bijective_preserves_J_eq_id_or_inv
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
eq_self_or_inv
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
ext
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
JAut
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
multiplicative
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
posHalf
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
posInv
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
posInv_inv
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
posMul
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
posOne
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
posTwo
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
preserves_cost
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
reciprocal_ne_id
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
two_mul_inv_eq_two_mul_iff
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
two_mul_inv_ne_inv_two_mul
in IndisputableMonolith.Algebra.CostAlgebra
decl_use