Code

Add mulGrp to iset.mm#4509

Code

Merged

jkingdon merged 20 commits intometamath:developmetamath/set.mm:developfrom jkingdon:mgpjkingdon/set.mm:mgpCopy head branch name to clipboardDec 30, 2024

+403-12

Commits

Commits on Dec 30, 2024

• Add lgsqr to mmil.html

  jkingdon

  committed
  7d91b08

• Add df-drng and df-field to mmil.html

  Show description for 44a6a5b
  jkingdon

  committed
  44a6a5b

• Add mulGrp to iset.mm

  Show description for 86d72df
  jkingdon

  committed
  86d72df

• Add fnmgp to iset.mm

  Show description for cc38465
  jkingdon

  committed
  cc38465

• Add mgpvalg to iset.mm

  Show description for 093b27b
  jkingdon

  committed
  093b27b

• Add mgpplusgg to iset.mm

  Show description for 5eeadcb
  jkingdon

  committed
  5eeadcb

• Add mgpbasg to iset.mm

  Show description for 1ba1fb0
  jkingdon

  committed
  1ba1fb0

• add setsplusg to mmil.html

  jkingdon

  committed
  d422fae

• Add slot theorems to iset.mm

  Show description for ea736b6
  jkingdon

  committed
  ea736b6

• Add mgpscag to iset.mm

  Show description for 2aa7130
  jkingdon

  committed
  2aa7130

• Add tset slot theorems to iset.mm

  Show description for adb236c
  jkingdon

  committed
  adb236c

• Add mgptsetg to iset.mm

  Show description for cf2badd
  jkingdon

  committed
  cf2badd

• Add mgptopng to iset.mm

  Show description for 99afe04
  jkingdon

  committed
  99afe04

• Add distance slot theorems to iset.mm

  Show description for 6caef98
  jkingdon

  committed
  6caef98

• Add mgpdsg to iset.mm

  Show description for 28795d2
  jkingdon

  committed
  28795d2

• add mgpress to mmil.html

  jkingdon

  committed
  049324c

• Add 1r (ring unit) to iset.mm

  Show description for 17a9351
  jkingdon

  committed
  17a9351

• Add ringidvalg to iset.mm

  Show description for 20472e1
  jkingdon

  committed
  20472e1

• Add dfur2g to iset.mm

  Show description for e9d9e77
  jkingdon

  committed
  e9d9e77

• Revise df-ur comment in iset.mm and set.mm

  Show description for 0227e9b
  jkingdon

  committed
  0227e9b