Skip to content

A revised attempt at ax-mulf comment wording #5032

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Oct 7, 2025
Merged

A revised attempt at ax-mulf comment wording #5032

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cd9e89b
Clarify ax-mulf comment
david-a-wheeler Apr 30, 2025
429a496
Revise wording of ax-mulf and axmulf
jkingdon Oct 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 12 additions & 15 deletions iset.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84297,10 +84297,10 @@ involve to natural numbers (notably, ~ axcaucvg ). (Contributed by
VAWPABGJJVBVCVRWDVDSABHIJKILZJNHLXFNHRSHXFVEVFWEWBSVTWAVGZVFWCKVHSXEKVIVP
VJVKVLKVRVMVNWBABJXGVOABJJJKVQVN $.

$( Multiplication is an operation on the complex numbers. This theorem can
be used as an alternate axiom for complex numbers in place of the less
specific ~ axmulcl . This construction-dependent theorem should not be
referenced directly; instead, use ~ ax-mulf . (Contributed by NM,
$( Multiplication is an operation on the complex numbers. This is the
construction-dependent version of ~ ax-mulf and it should not be
Comment on lines +84300 to +84301
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should ax-mulf be mulcl here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, this sentence is contrasting ax-mulf and axmulf. The following sentence is about axmulf (or ax-mulf) versus mulcl

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't really understand how one theorem is the construction-dependent version of the other when they're both the same - by my understanding both are construction-dependent.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The "construction-dependent" wording is not new and is used throughout this section (see for example https://us.metamath.org/mpeuni/ax1cn.html ).

We could consider that phrasing in another issue or pull request; I'm not sure I have an immediate thought about alternate wordings for this $j restatement situation.

Copy link
Contributor

@icecream17 icecream17 Oct 6, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah I see, I mixed up the notion of the result of axmulf/ax-mulf as a property depending on the certain definition of multiplication, vs whether axmulf/ax-mulf is proven from, i.e. dependent on, the construction of complex numbers or stated as an axiom.

The wording makes sense now

referenced outside the construction. We generally prefer to develop our
theory using the less specific ~ mulcl . (Contributed by NM,
8-Feb-2005.) (New usage is discouraged.) $)
axmulf $p |- x. : ( CC X. CC ) --> CC $=
( vx vy vw vv vu vf vz vb va cc cmul cv co wcel wceq wa cop cmr wex wtru
Expand Down Expand Up @@ -85486,17 +85486,14 @@ this axiom (with the defined operation in place of ` + ` ) follows as a
ax-addf $a |- + : ( CC X. CC ) --> CC $.
$( $j restatement 'ax-addf' of 'axaddf'; $)

$( Multiplication is an operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first- or second-order statement (see
~ https://us.metamath.org/downloads/schmidt-cnaxioms.pdf ). It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ~ ax-mulcl should be used. Note that uses of ~ ax-mulf
can be eliminated by using the defined operation
` ( x e. CC , y e. CC |-> ( x x. y ) ) ` in place of ` x. ` , from which
this axiom (with the defined operation in place of ` x. ` ) follows as a
theorem.
$( Multiplication is an operation on the complex numbers. This axiom tells
us that ` x. ` is defined only on complex numbers which is analogous to
the way that other operations are defined, for example see ~ subf or
~ eff . However, while Metamath can handle this axiom, if we wish to work
with weaker complex number axioms, we can avoid it by using the less
specific ~ mulcl . Note that uses of ~ ax-mulf can be eliminated by using
the defined operation ` ( x e. CC , y e. CC |-> ( x x. y ) ) ` in place of
` x. ` , as seen in ~ mpomulf .

This axiom is justified by Theorem ~ axmulf . (New usage is discouraged.)
(Contributed by NM, 19-Oct-2004.) $)
Expand Down
27 changes: 12 additions & 15 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127715,10 +127715,10 @@ the converse membership relation (which is not an equivalence relation)
YCXLMXQXSXRXTYFXQXSTYDXRXTTYEWQWLVHWKWNVHVIVNYBWRSSVJVOVKVLVEVMZVPVQJWBVR
VSWGABHHYGVTABHHHJWAVS $.

$( Multiplication is an operation on the complex numbers. This theorem can
be used as an alternate axiom for complex numbers in place of the less
specific ~ axmulcl . This construction-dependent theorem should not be
referenced directly; instead, use ~ ax-mulf . (Contributed by NM,
$( Multiplication is an operation on the complex numbers. This is the
construction-dependent version of ~ ax-mulf and it should not be
referenced outside the construction. We generally prefer to develop our
theory using the less specific ~ mulcl . (Contributed by NM,
8-Feb-2005.) (New usage is discouraged.) $)
axmulf $p |- x. : ( CC X. CC ) --> CC $=
( vx vy vw vv vu vf vz cc cmul cv co wcel wceq wa cop cmr wex cnr mulclsr
Expand Down Expand Up @@ -128361,17 +128361,14 @@ this axiom (with the defined operation in place of ` + ` ) follows as a
ax-addf $a |- + : ( CC X. CC ) --> CC $.
$( $j restatement 'ax-addf' of 'axaddf'; $)

$( Multiplication is an operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first-order or second-order statement (see
~ https://us.metamath.org/downloads/schmidt-cnaxioms.pdf ). It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ~ ax-mulcl should be used. Note that uses of ~ ax-mulf
can be eliminated by using the defined operation
` ( x e. CC , y e. CC |-> ( x x. y ) ) ` in place of ` x. ` , from which
this axiom (with the defined operation in place of ` x. ` ) follows as a
theorem.
$( Multiplication is an operation on the complex numbers. This axiom tells
us that ` x. ` is defined only on complex numbers which is analogous to
the way that other operations are defined, for example see ~ subf or
~ eff . However, while Metamath can handle this axiom, if we wish to work
with weaker complex number axioms, we can avoid it by using the less
specific ~ mulcl . Note that uses of ~ ax-mulf can be eliminated by using
the defined operation ` ( x e. CC , y e. CC |-> ( x x. y ) ) ` in place of
` x. ` , as seen in ~ mpomulf .

This axiom is justified by Theorem ~ axmulf . (New usage is discouraged.)
(Contributed by NM, 19-Oct-2004.) $)
Expand Down