Search results

Intermediate value theorem is equivalent to (some constructive taboo)

Status: Open.

#4918 In metamath/set.mm;

· jkingdon opened on Jun 29, 2025

Find a better definition of df-gsum for iset.mm

Status: Open.

#4914 In metamath/set.mm;

· jkingdon opened on Jun 25, 2025

Inconsistency ?

Status: Open.

#4904 In metamath/set.mm;

· tirix opened on Jun 20, 2025

Status of syl related renames

Status: Open.

#4902 In metamath/set.mm;

· jkingdon opened on Jun 19, 2025

Define cyclotomic fields

Status: Open.

#4896 In metamath/set.mm;

· icecream17 opened on Jun 15, 2025

Spellchecking in <code>set.mm</code> (and <code>iset.mm</code>)

Status: Open.

#4875 In metamath/set.mm;

· tirix opened on Jun 5, 2025

Define polynomials in iset.mm

Status: Open.

#4846 In metamath/set.mm;

· jkingdon opened on May 23, 2025

(Local) Isomorphisms of graphs

Status: Open.

#4808 In metamath/set.mm;

· avekens opened on May 4, 2025

Add Myhill isomorphism theorem to iset.mm

Status: Open.

#4802 In metamath/set.mm;

· jkingdon opened on May 2, 2025

Typo in description of Theorem ceqsexgv?

Status: Open.

#4695 In metamath/set.mm;

· billh0420 opened on Mar 6, 2025

Generalize evls1rhm from CRing to Ring

Status: Open.

#4658 In metamath/set.mm;

· icecream17 opened on Feb 15, 2025

Rename 2p2e4 et al?

Status: Open.

#4624 In metamath/set.mm;

· icecream17 opened on Feb 2, 2025