Skip to content

Commit 1314c60

Browse files
committed
[delete] assascacom and assascacrng
1 parent cd896ee commit 1314c60

File tree

1 file changed

+0
-21
lines changed

1 file changed

+0
-21
lines changed

set.mm

Lines changed: 0 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -835249,27 +835249,6 @@ have GLB (expanded version). (Contributed by Zhi Wang,
835249835249
$}
835250835250
$}
835251835251

835252-
${
835253-
assascacom.f $e |- F = ( Scalar ` W ) $.
835254-
assascacom.b $e |- B = ( Base ` F ) $.
835255-
assascacom.m $e |- .* = ( .r ` F ) $.
835256-
assascacom.w $e |- ( ph -> W e. AssAlg ) $.
835257-
assascacom.a $e |- ( ph -> A e. B ) $.
835258-
assascacom.c $e |- ( ph -> C e. B ) $.
835259-
$( The scalars of an associative algebra are commutative. This is actually
835260-
false. See ~ asclcom . (Contributed by Zhi Wang, 11-Sep-2025.) $)
835261-
assascacom $p |- ( ph -> ( A .* C ) = ( C .* A ) ) $=
835262-
( ) ? $.
835263-
$}
835264-
835265-
${
835266-
assascacrng.f $e |- F = ( Scalar ` W ) $.
835267-
$( The scalars of an associative algebra are commutative. This is actually
835268-
false. See ~ asclcom . (Contributed by Zhi Wang, 11-Sep-2025.) $)
835269-
assascacrng $p |- ( W e. AssAlg -> F e. CRing ) $=
835270-
( ) ? $.
835271-
$}
835272-
835273835252

835274835253
$(
835275835254
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

0 commit comments

Comments
 (0)